Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / 04_Complement
Bitbucket
Dashboard
チーム
リポジトリ
Snippets
owner/repository
Logged in as HirokazuYatsu
2
3
Wiki CafeOBJ / OSEK / contents / index-e / 04_Complement 表示 履歴 編集 削除 タイトルrequired ページの内容
Complement of Invresed Relation
In this section, we introduce two modules. One is a module to extend a relation on a set to that on a powerset. The other is a module to produce the complement of the inverse of a given relation.
EXTEND
Let R be an arbitrary binary relation on a set S. The module EXTEND enables us to extend R to a relation on the powerset of S.
#!python module EXTEND ( X :: TRIV, C :: SET(X), R :: RELATION(X) ) { imports { ex(DEDUCIBLE) } signature { op ___ : Set Relation Set -> Prop } axioms { vars X Y : Elt vars S U V : Set vars R : Relation cq S R nil = true if neg(S = nil) . eq nil R S = false . -- (S R (U,V)) = (S R U)/\(S R V) eq deducible((S R (U,V)) |- (S R U)) = true . eq deducible((S R U),(S R V) |- (S R (U,V))) = true . -- ((U,V) R S) = (U R S)\/(V R S) eq deducible(((U,V) R S) |- (U R S),(V R S)) = true . eq deducible((U R S) |- ((U,V) R S)) = true . } }
COMPLEMENT
The module COMPLEMENT is to declare a function which returns the complement of the inverse of a given relation.
Let R be an arbitrary relation on a set S. Then, the relation [R] represents the complement of the inverse of R. For any x,y∈S,
- x [R] y ⇔ ¬(y R x)
#!python module COMPLEMENT ( X :: TRIV, R :: RELATION(X) ) { imports { ex(DEDUCIBLE) } signature { op [_] : Relation -> Relation } axioms { vars X Y : Elt vars R : Relation -- X [R] Y = (neg Y R X) . eq deducible((X [R] Y),(Y R X) |- nil) = true . eq deducible(nil |- (X [R] Y),(Y R X)) = true . } }
LEMMA1/COMPLEMENT
For any irreflexive relation R, the complement of its reverse [R] is also irreflexive. This claim can be declared as the following module.
#!python module CLAIM1/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), I :: IRREFLEXIVE(X,R) ) { imports { pr(LK) pr(COMPLEMENT(X,R)) } signature { op r : -> Irreflexive op x : -> Elt op claim : -> Prop } axioms { eq claim = deducible(nil |- (x [r] x)) . } }
#!python open CLAIM1/COMPLEMENT . ops q1 q2 : -> Sequent . eq q1 = (nil |- (x [r] x),(x r x)) . eq q2 = ((x r x) |- nil) . ops i : -> Inference . eq antecedent(i) = (q1,q2) . eq (nil |- (x [r] x)) = consequent(i) . red claim . close
#!python -- reduce in %CLAIM1/COMPLEMENT(X, S, R, I) : (claim):Prop ** Found [state 3] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 30 rewrites(0.010 sec), 217 matches, 1 memo hits)
module LEMMA1/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), I :: IRREFLEXIVE(X,R), C :: COMPLEMENT(X,R) ) { imports { pr(LK) } axioms { vars X : Elt vars R : Irreflexive eq deducible(nil |- (X [R] X)) = true . } }
LEMMA2/COMPLEMENT
For any asymmetric relation R on a set S, the complement of the inverse of R becomes to be total, i.e.,
- ∀s⊆S,x∈S・(x [R] s)∨(s [R] x)
#!python module CLAIM2/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), A :: ASYMMETRIC(X,R) ) { imports { pr(LK) pr(COMPLEMENT(X,R)) pr(EXTEND(X,S,R)) } signature { op x : -> Elt op r : -> Asymmetric op claim : Set -> Prop } axioms { vars S : Set eq claim(S) = deducible(nil |- ((x [r] S),(S [r] x))) . } }
#!python -- [base case] open CLAIM2/COMPLEMENT . red claim(nil) . close -- [induction step] open CLAIM2/COMPLEMENT . ops s n : -> Set . ops y : -> Elt . eq n = (s,y) . -- [induction hypothesis] eq deducible(nil |- ((x [r] s),(s [r] x))) = true . -- under the hypothesis, claim(n) is reduced to be true ops q1 q2 q3 q4 q5 q6 q7 : -> Sequent . -- asymmetricity of r eq q1 = ((x r y),(y r x) |- nil) . -- definitions of the complement of r eq q2 = (nil |- (x [r] y),(y r x)) . eq q3 = (nil |- (y [r] x),(x r y)) . -- asummption of induction eq q4 = (nil |- (x [r] s),(s [r] x)) . -- definition of extention of [r] eq q5 = ((x [r] s),(x [r] y) |- (x [r] n)) . eq q6 = ((s [r] x) |- (n [r] x)) . eq q7 = ((y [r] x) |- (n [r] x)) . ops i1 i2 i3 : -> Inference . eq antecedent(i1) = (q1,q2,q3) . trans (nil |- (x [r] y),(y [r] x)) => consequent(i1) . trans consequent(i1) => (nil |- (x [r] y),(y [r] x)) . eq antecedent(i2) = (consequent(i1),q4,q5) . trans (nil |- (x [r] (s,y)),(s [r] x),(y [r] x)) => consequent(i2) . trans consequent(i2) => (nil |- (x [r] (s,y)),(s [r] x),(y [r] x)) . eq antecedent(i3) = (consequent(i2),q6,q7) . eq (nil |- ((x [r] (s,y)),((s,y) [r] x))) = consequent(i3) . red claim(n) . close
#!python -- opening module CLAIM2/COMPLEMENT(X, S, R, A).. done. -- reduce in %CLAIM2/COMPLEMENT(X, S, R, A) : (claim(nil)):Prop (true):Bool (0.000 sec for parse, 6 rewrites(0.000 sec), 41 matches) -- opening module CLAIM2/COMPLEMENT(X, S, R, A).. done. ___* -- reduce in %CLAIM2/COMPLEMENT(X, S, R, A) : (claim(n)):Prop ** Found [state 719] (consequent(i3)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 1240] (consequent(i2)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 268] (consequent(i1)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 32388 rewrites(13.420 sec), 1786294 matches, 18344 memo hits)
#!python module LEMMA2/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), A :: ASYMMETRIC(X,R), C :: COMPLEMENT(X,R), E :: EXTEND(X,S,R) ) { imports { pr(LK) } axioms { vars S : Set vars X : Elt vars R : Asymmetric eq deducible(nil |- ((X [R] S),(S [R] X))) = true . } }
LEMMA3/COMPLEMENT
For any transitive relation R on a set S, the following traisitivity holds:
- ∀x,y∈S・∀s⊆S・(x R y)∧(y [R] s) ⇒ (x [R] s)
#!python module CLAIM3/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), T :: TRANSITIVE(X,R) ) { imports { pr(LK) pr(COMPLEMENT(X,R)) pr(EXTEND(X,S,R)) } signature { ops x y : -> Elt op r : -> Transitive op claim : Set -> Prop } axioms { vars S : Set eq claim(S) = deducible((x r y),(y [r] S) |- (x [r] S)) . } }
#!python -- [base case] open CLAIM3/COMPLEMENT . red claim(nil) . close -- [induction step] open CLAIM3/COMPLEMENT . ops c n : -> Set . ops z : -> Elt . eq n = c,z . -- [induction hypothesis] eq deducible((x r y),(y [r] c) |- (x [r] c)) = true . ops q1 q2 q3 q4 q5 q6 q7 : -> Sequent . -- transitivity of r eq q1 = ((z r x),(x r y) |- (z r y)) . -- definition of complement eq q2 = ((y [r] z),(z r y) |- nil) . eq q3 = (nil |- (x [r] z),(z r x)) . -- hypothesis of induction eq q4 = ((x r y),(y [r] c) |- (x [r] c)) . -- definitions of extension eq q5 = ((x [r] z),(x [r] c) |- (x [r] n)) . eq q6 = ((y [r] n) |- (y [r] z)) . eq q7 = ((y [r] n) |- (y [r] c)) . ops i1 i2 i3 i4 : -> Inference . eq antecedent(i1) = (q1,q2,q3) . trans ((x r y),(y [r] z) |- (x [r] z)) => consequent(i1) . trans consequent(i1) => ((x r y),(y [r] z) |- (x [r] z)) . eq antecedent(i2) = (consequent(i1),q5) . trans ((x r y),(y [r] z),(x [r] c) |- (x [r] (c,z))) => consequent(i2) . trans consequent(i2) => ((x r y),(y [r] z),(x [r] c) |- (x [r] (c,z))) . eq antecedent(i3) = (consequent(i2),q4) . trans ((x r y),(y [r] z),(y [r] c) |- (x [r] (c,z))) => consequent(i3) . trans consequent(i3) => ((x r y),(y [r] z),(y [r] c) |- (x [r] (c,z))) . eq antecedent(i4) = (consequent(i3),q6,q7) . eq ((x r y),(y [r] (c,z)) |- (x [r] (c,z))) = consequent(i4) . red claim(n) . close
#!python -- opening module CLAIM3/COMPLEMENT(X, S, R, T).. done. -- reduce in %CLAIM3/COMPLEMENT(X, S, R, T) : (claim(nil)):Prop (true):Bool (0.000 sec for parse, 14 rewrites(0.000 sec), 154 matches) -- opening module CLAIM3/COMPLEMENT(X, S, R, T).. done. ___* -- reduce in %CLAIM3/COMPLEMENT(X, S, R, T) : (claim(n)):Prop ** Found [state 1366] (consequent(i4)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 267] (consequent(i3)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 179] (consequent(i2)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 376] (consequent(i1)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 23159 rewrites(12.780 sec), 1304434 matches, 12495 memo hits)
#!python module LEMMA3/COMPLEMENT ( X :: TRIV, S :: SET(X), R :: RELATION(X), T :: TRANSITIVE(X,R), C :: COMPLEMENT(X,R), E :: EXTEND(X,S,R) ) { imports { pr(LK) } axioms { vars X Y : Elt vars R : Transitive vars S : Set eq deducible((X R Y),(Y [R] S) |- (X [R] S)) = true . } }
LEMMA4/COMPLEMENT
For any asymmetric relation R on a set S, the complement of the inverse of R includes R itself.
- ∀x,y∈S・(x R y) ⇒ (x [R] y)
This claim can be represented as the following module:
#!python module CLAIM4/COMPLEMENT ( X :: TRIV, R :: RELATION(X), A :: ASYMMETRIC(X,R) ) { imports { pr(LK) pr(COMPLEMENT(X,R)) } signature { ops x y : -> Elt op r : -> Asymmetric op claim : -> Prop } axioms { eq claim = deducible((x r y) |- (x [r] y)) . } }
#!python open CLAIM4/COMPLEMENT . ops q1 q2 : -> Sequent . eq q1 = ((x r y),(y r x) |- nil) . eq q2 = (nil |- (x [r] y),(y r x)) . ops i : -> Inference . eq antecedent(i) = (q1,q2) . eq ((x r y) |- (x [r] y)) = consequent(i) . red claim . close
#!python -- opening module CLAIM4/COMPLEMENT(X, R, A).. done. __* -- reduce in %CLAIM4/COMPLEMENT(X, R, A) : (claim):Prop ** Found [state 1] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 42 rewrites(0.000 sec), 412 matches, 7 memo hits)
#!python module LEMMA4/COMPLEMENT ( X :: TRIV, R :: RELATION(X), A :: ASYMMETRIC(X,R), C :: COMPLEMENT(X,R) ) { imports { pr(LK) } axioms { vars X Y : Elt vars R : Asymmetric eq deducible((X R Y) |- (X [R] Y)) = true . } }
LEMMA5/COMPLEMENT
Let (S,R) be an arbitrary totally ordered set. Then the following three properties on transitivity hold.
- ∀x,y,z∈S・(x [R] y)∧(y R z) ⇒ (x R z)
- ∀x,y,z∈S・(x R y)∧(y [R] z) ⇒ (x R z)
- ∀x,y,z∈S・(x [R] y)∧(y [R] z) ⇒ (x [R] z)
#!python module CLAIM5/COMPLEMENT ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), V :: TRANSITIVE(X,R), P :: PARTIALORDER(X,R,I,A,V), T :: TOTALORDER(X,R,I,A,V,P) ) { imports { pr(LEMMA1/TOTALORDER(X,R,I,A,V,P,T)) pr(COMPLEMENT(X,R)) } signature { ops x y z : -> Elt op r : -> TotalOrder ops claim1 claim2 claim3 : -> Prop } axioms { eq claim1 = deducible((x [r] y),(y r z) |- (x r z)) . eq claim2 = deducible((x r y),(y [r] z) |- (x r z)) . eq claim3 = deducible((x [r] y),(y [r] z) |- (x [r] z)) . } }
#!python open CLAIM5/COMPLEMENT . ops q1 q2 : -> Sequent . eq q1 = ((y r z) |- (x r z),(y r x)) . eq q2 = ((x [r] y),(y r x) |- nil) . ops i : -> Inference . eq antecedent(i) = (q1,q2) . eq ((x [r] y),(y r z) |- (x r z)) = consequent(i) . red claim1 . close -- open CLAIM5/COMPLEMENT . ops q1 q2 : -> Sequent . eq q1 = ((x r y) |- (x r z),(z r y)) . eq q2 = ((y [r] z),(z r y) |- nil) . ops i : -> Inference . eq antecedent(i) = (q1,q2) . eq ((x r y),(y [r] z) |- (x r z)) = consequent(i) . red claim2 . close -- open CLAIM5/COMPLEMENT . ops q1 q2 q3 q4 : -> Sequent . eq q1 = ((z r x) |- (y r x),(z r y)) . eq q2 = ((x [r] y),(y r x) |- nil) . eq q3 = ((y [r] z),(z r y) |- nil) . eq q4 = (nil |- (x [r] z),(z r x)) . ops i : -> Inference . eq antecedent(i) = (q1,q2,q3,q4) . eq ((x [r] y),(y [r] z) |- (x [r] z)) = consequent(i) . red claim3 . close
#!python -- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done. __* -- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : (claim1):Prop ** Found [state 1] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 47 rewrites(0.000 sec), 676 matches, 7 memo hits) -- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done. __* -- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : (claim2):Prop ** Found [state 1] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 47 rewrites(0.000 sec), 676 matches, 7 memo hits) -- opening module CLAIM5/COMPLEMENT(X, R, I, A, V, P, T).. done. __* -- reduce in %CLAIM5/COMPLEMENT(X, R, I, A, V, P, T) : (claim3):Prop ** Found [state 982] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 47936 rewrites(45.600 sec), 2301887 matches, 30145 memo hits)
#!python module LEMMA5/COMPLEMENT ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), V :: TRANSITIVE(X,R), P :: PARTIALORDER(X,R,I,A,V), T :: TOTALORDER(X,R,I,A,V,P), C :: COMPLEMENT(X,R) ) { imports { pr(LK) } axioms { vars X Y Z : Elt vars R : TotalOrder eq deducible((X [R] Y),(Y R Z) |- (X R Z)) = true . eq deducible((X R Y),(Y [R] Z) |- (X R Z)) = true . eq deducible((X [R] Y),(Y [R] Z) |- (X [R] Z)) = true . } }
コミットメッセージ キャンセル
ブログ サポート Plans & pricing ドキュメント API Site status Version info サービス利用規約 プライバシー ポリシー
JIRA Confluence Bamboo SourceTree HipChat
Atlassian
Updated