Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / 07_Override
Override of Relations
OVERRIDE
#!python module OVERRIDE ( X :: TRIV, R :: RELATION(X) ) { signature { op [_;_] : Relation Relation -> Relation } axioms { vars F G : Relation vars X Y : Elt eq deducible((X F Y) |- (X [F;G] Y)) = true . eq deducible((X G Y) |- ((Y F X),(X [F;G] Y))) = true . eq deducible((X [F;G] Y) |- ((X F Y),(X G Y))) = true . eq deducible((X [F;G] Y),(Y F X) |- (X F Y)) = true . } }
CLAIM1/OVERRIDE
#!python module CLAIM1/OVERRIDE ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R) ) { imports { pr(LK) pr(OVERRIDE(X,R)) } signature { op x : -> Elt ops f g : -> Irreflexive ops claim : -> Prop } axioms { eq claim = (x [f;g] x |- nil) . } }
SCORE/CLAIM1/OVERRIDE
#!python open CLAIM1/OVERRIDE . ops q1 q2 q3 : -> Sequent . eq q1 = ((x f x) |- nil) . eq q2 = ((x g x) |- nil) . eq q3 = ((x [f;g] x) |- ((x f x),(x g x))) . ops i : -> Inference . eq antecedent(i) = (q1,q2,q3) . eq ((x [f;g] x) |- nil) = consequent(i) . red deducible((x [f;g] x) |- nil) . close
#!python -- opening module CLAIM1/OVERRIDE(X, R, I).. done. __* -- reduce in %CLAIM1/OVERRIDE(X, R, I) : (deducible(((x ([ f ; g ]) x) |- nil))):Prop ** Found [state 51] (consequent(i)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 195 rewrites(0.130 sec), 4960 matches, 64 memo hits)
CLAIM2/OVERRIDE
#!python module CLAIM2/OVERRIDE ( X :: TRIV, R :: RELATION(X), A :: ASYMMETRIC(X,R) ) { imports { pr(LK) pr(OVERRIDE(X,R)) } signature { ops x y : -> Elt ops f g : -> Asymmetric ops claim : -> Prop } axioms { eq claim = ((x [f;g] y),(y [f;g] x) |- nil) . } }
SCORE/CLAIM2/OVERRIDE
#!python open CLAIM2/OVERRIDE . ops q1 q2 q3 q4 q5 q6 : -> Sequent . eq q1 = ((x f y),(y f x)) |- nil . eq q2 = ((x g y),(y g x)) |- nil . eq q3 = (x [f;g] y) |- ((x f y),(x g y)) . eq q4 = (y [f;g] x) |- ((y f x),(y g x)) . eq q5 = ((x [f;g] y),(y f x)) |- (x f y) . eq q6 = ((y [f;g] x),(x f y)) |- (y f x) . ops i1 i2 i3 i4 i5 : -> Inference . eq antecedent(i1) = (q1,q6) . trans (((y [f;g] x),(x f y)) |- nil) => consequent(i1) . trans consequent(i1) => (((y [f;g] x),(x f y)) |- nil) . eq antecedent(i2) = (q4,q5) . trans (((x [f;g] y),(y [f;g] x)) |- ((x f y),(y g x))) => consequent(i2) . trans consequent(i2) => (((x [f;g] y),(y [f;g] x)) |- ((x f y),(y g x))) . eq antecedent(i3) = (consequent(i2),q3) . trans (((x [f;g] y),(y [f;g] x)) |- ((x f y),((x g y)/\(y g x)))) => consequent(i3) . trans consequent(i3) => (((x [f;g] y),(y [f;g] x)) |- ((x f y),((x g y)/\(y g x)))) . eq antecedent(i4) = (consequent(i3),q2) . trans (((x [f;g] y),(y [f;g] x)) |- (x f y)) => consequent(i4) . trans consequent(i4) => (((x [f;g] y),(y [f;g] x)) |- (x f y)) . eq antecedent(i5) = (consequent(i1),consequent(i4)) . eq (((x [f;g] y),(y [f;g] x)) |- nil) = consequent(i5) . red deducible(((x [f;g] y),(y [f;g] x)) |- nil) . close
#!python -- opening module CLAIM2/OVERRIDE(X, R, A).. done. __* -- reduce in %CLAIM2/OVERRIDE(X, R, A) : (deducible((((x ([ f ; g ]) y) , (y ([ f ; g ]) x)) |- nil))):Prop ** Found [state 26] (consequent(i5)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 2009] (consequent(i4)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 97] (consequent(i3)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 23] (consequent(i2)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 67] (consequent(i1)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 7465 rewrites(5.580 sec), 281375 matches, 3919 memo hits)
CLAIM3/OVERRIDE
#!python module CLAIM3/OVERRIDE ( X :: TRIV, R :: RELATION(X), A :: ASYMMETRIC(X,R) ) { imports { pr(LK) pr(COMPLEMENT(X,R)) pr(OVERRIDE(X,R)) } signature { ops x y : -> Elt ops f : -> Asymmetric ops g : -> Relation ops claim : -> Prop } axioms { eq claim = deducible((x [f;g] y) |- (x [f] y)) . } }
SCORE/CLAIM3/OVERRIDE
#!python open CLAIM3/OVERRIDE . ops q1 q2 q3 : -> Sequent . eq q1 = ((x f y),(y f x) |- nil) . eq q2 = (nil |- (y f x),(x [f] y)) . eq q3 = ((x [f;g] y),(y f x) |- (x f y)) . ops i1 i2 : -> Inference . eq antecedent(i1) = (q1,q3) . trans ((x [f;g] y),(y f x) |- nil) => consequent(i1) . trans consequent(i1) => ((x [f;g] y),(y f x) |- nil) . eq antecedent(i2) = (consequent(i1),q2) . eq ((x [f;g] y) |- x [f] y) = consequent(i2) . red claim . close
#!python -- opening module CLAIM3/OVERRIDE(X, R, A).. done. __* -- reduce in %CLAIM3/OVERRIDE(X, R, A) : (claim):Prop ** Found [state 5] (consequent(i2)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 67] (consequent(i1)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 400 rewrites(0.150 sec), 8569 matches, 150 memo hits)
CLAIM4/OVERRIDE
#!python module CLAIM4/OVERRIDE ( X :: TRIV, R :: RELATION(X), C :: COMPLEMENT(X,R) ) { imports { pr(LK) pr(OVERRIDE(X,R)) } signature { ops x y : -> Elt ops f g : -> Relation ops claim1 claim2 : -> Prop } axioms { eq claim1 = deducible((x [f;g] y) |- (x f y),((x g y) /\ (x [f] y))) . eq claim2 = deducible((x g y),(x [f] y) |- (x [f;g] y)) . } }
SCORE/CLAIM4/OVERRIDE
#!python open CLAIM4/OVERRIDE . ops q1 q2 q3 : -> Sequent . eq q1 = ((x [f;g] y) |- (x f y),(x g y)) . eq q2 = ((x [f;g] y),(y f x) |- (x f y)) . eq q3 = (nil |- (x [f] y),(y f x)) . ops i : -> Inference . eq antecedent(i) = (q1,q2,q3) . eq ((x [f;g] y) |- (x f y),((x g y) /\ (x [f] y))) = consequent(i) . red claim1 . close open CLAIM4/OVERRIDE . ops q1 q2 : -> Sequent . eq q1 = ((x g y) |- ((y f x),(x [f;g] y))) . eq q2 = ((x [f] y),(y f x) |- nil) . ops i : -> Inference . eq antecedent(i) = (q1,q2) . eq ((x g y),(x [f] y) |- (x [f;g] y)) = consequent(i) . red claim2 . close
#!python -- opening module CLAIM4/OVERRIDE(X, R, C).. done. __* -- reduce in %CLAIM4/OVERRIDE(X, R, C) : (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.010 sec), 673 matches, 7 memo hits)
OVERRIDE/REV1
#!python module OVERRIDE ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), C :: COMPLEMENT(X,R) ) { signature { op [_;_] : Relation Relation -> Relation op [_;_] : Irreflexive Irreflexive -> Irreflexive op [_;_] : Asymmetric Asymmetric -> Asymmetric } axioms { vars F G : Relation vars X Y : Elt vars R : Asymmetric eq deducible((X F Y) |- (X [F;G] Y)) = true . eq deducible((X G Y) |- ((Y F X),(X [F;G] Y))) = true . eq deducible((X [F;G] Y) |- ((X F Y),(X G Y))) = true . eq deducible((X [F;G] Y),(Y F X) |- (X F Y)) = true . eq deducible((X [R;G] Y) |- (X [R] Y)) = true . eq deducible((X [F;G] Y) |- (X F Y),((X G Y) /\ (X [F] Y))) = true . eq deducible((X G Y),(X [F] Y) |- (X [F;G] Y)) = true . } }
CLAIM5/OVERRIDE
#!python module CLAIM5/OVERRIDE ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), T :: TRANSITIVE(X,R), C :: COMPLEMENT(X,R) ) { imports { pr(LK) pr(OVERRIDE(X,R,I,A,C)) } signature { ops x y z : -> Elt ops f g : -> Transitive ops claim : -> Prop } axioms { vars X Y Z : Elt eq deducible((X f Y) |- (X f Z),(Z f Y)) = true . eq deducible((X [f] Y),(Y f Z) |- (X f Z)) = true . eq deducible((X f Y),(Y [f] Z) |- (X f Z)) = true . eq deducible((X [f] Y),(Y [f] Z) |- (X [f] Z)) = true . eq claim = deducible((x [f;g] y),(y [f;g] z) |- (x [f;g] z)) . } }
SCORE/CLAIM5/OVERRIDE
#!python open CLAIM5/OVERRIDE . ops r : -> Relation . eq r = [f;g] . ops q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 : -> Sequent . eq q1 = (nil |- (y f x),(x [f] y)) . eq q2 = (nil |- (z f y),(y [f] z)) . eq q3 = ((x f y),(y f z) |- (x f z)) . eq q4 = ((x f y),(y [f] z) |- (x f z)) . eq q5 = ((x [f] y),(y f z) |- (x f z)) . eq q6 = ((x [f] y),(y [f] z) |- (x [f] z)) . eq q7 = ((x g y),(y g z) |- (x g z)) . eq q8 = ((x f z) |- (x r z)) . eq q9 = ((x r y),(y f x) |- (x f y)) . eq q10 = ((y r z),(z f y) |- (y f z)) . eq q11 = ((x g z),(x [f] z) |- (x r z)) . eq q12 = ((x r y) |- (x f y),((x g y) /\ (x [f] y))) . eq q13 = ((y r z) |- (y f z),((y g z) /\ (y [f] z))) . ops i1 : -> Inference . eq antecedent(i1) = (q1,q9) . trans ((x [f;g] y) |- (x f y),(x [f] y)) => consequent(i1) . trans consequent(i1) => ((x [f;g] y) |- (x f y),(x [f] y)) . ops i2 : -> Inference . eq antecedent(i2) = (q2,q10) . trans ((y [f;g] z) |- (y f z),(y [f] z)) => consequent(i2) . trans consequent(i2) => ((y [f;g] z) |- (y f z),(y [f] z)) . ops i3 : -> Inference . eq antecedent(i3) = (q7,q11) . trans ((x g y),(y g z),(x [f] z) |- (x [f;g] z)) => consequent(i3) . trans consequent(i3) => ((x g y),(y g z),(x [f] z) |- (x [f;g] z)) . ops i4 : -> Inference . eq antecedent(i4) = (consequent(i3),q6) . trans ((x g y),(x [f] y),(y g z),(y [f] z) |- (x [f;g] z)) => consequent(i4) . trans consequent(i4) => ((x g y),(x [f] y),(y g z),(y [f] z) |- (x [f;g] z)) . ops i5 : -> Inference . eq antecedent(i5) = (consequent(i4),q12) . trans ((x [f;g] y),(y g z),(y [f] z) |- (x f y),(x [f;g] z)) => consequent(i5) . trans consequent(i5) => ((x [f;g] y),(y g z),(y [f] z) |- (x f y),(x [f;g] z)) . ops i6 : -> Inference . eq antecedent(i6) = (consequent(i5),q13) . trans ((x [f;g] y),(y [f;g] z) |- (x f y),(y f z),(x [f;g] z)) => consequent(i6) . trans consequent(i6) => ((x [f;g] y),(y [f;g] z) |- (x f y),(y f z),(x [f;g] z)) . ops i7 : -> Inference . eq antecedent(i7) = (consequent(i1),q5) . trans ((x [f;g] y),(y f z) |- (x f y),(x f z)) => consequent(i7) . trans consequent(i7) => ((x [f;g] y),(y f z) |- (x f y),(x f z)) . ops i8 : -> Inference . eq antecedent(i8) = (consequent(i6),consequent(i7)) . trans ((x [f;g] y),(y [f;g] z) |- (x f y),(x f z),(x [f;g] z)) => consequent(i8) . trans consequent(i8) => ((x [f;g] y),(y [f;g] z) |- (x f y),(x f z),(x [f;g] z)) . ops i9 : -> Inference . eq antecedent(i9) = (consequent(i2),q4) . trans ((x f y),(y [f;g] z) |- (x f z),(y f z)) => consequent(i9) . trans consequent(i9) => ((x f y),(y [f;g] z) |- (x f z),(y f z)) . ops i10 : -> Inference . eq antecedent(i10) = (consequent(i6),consequent(i9)) . trans ((x [f;g] y),(y [f;g] z) |- (y f z),(x f z),(x [f;g] z)) => consequent(i10) . trans consequent(i10) => ((x [f;g] y),(y [f;g] z) |- (y f z),(x f z),(x [f;g] z)) . ops i11 : -> Inference . eq antecedent(i11) = (consequent(i8),q3) . trans ((x [f;g] y),(y [f;g] z),(y f z) |- (x f z),(x [f;g] z)) => consequent(i11) . trans consequent(i11) => ((x [f;g] y),(y [f;g] z),(y f z) |- (x f z),(x [f;g] z)) . ops i12 : -> Inference . eq antecedent(i12) = (consequent(i10),consequent(i11)) . trans ((x [f;g] y),(y [f;g] z) |- (x f z),(x [f;g] z)) => consequent(i12) . trans consequent(i12) => ((x [f;g] y),(y [f;g] z) |- (x f z),(x [f;g] z)) . ops i13 : -> Inference . eq antecedent(i13) = (consequent(i12),q8) . eq ((x [f;g] y),(y [f;g] z) |- (x [f;g] z)) = consequent(i13) . red claim . close
#!python -- opening module CLAIM5/OVERRIDE(X, R, I, A, T, C).. done. _______________* -- reduce in %CLAIM5/OVERRIDE(X, R, I, A, T, C) : (claim):Prop ** Found [state 13] (consequent(i13)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 1457] (consequent(i12)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 63] (consequent(i11)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 1296] (consequent(i8)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 48] (consequent(i7)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 17] (consequent(i1)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 9383] (consequent(i6)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 8714] (consequent(i5)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 302] (consequent(i4)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 154] (consequent(i3)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 1296] (consequent(i10)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 48] (consequent(i9)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 17] (consequent(i2)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 9383] (consequent(i6)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 8714] (consequent(i5)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 302] (consequent(i4)):Set/Sequent {} -- found required number of solutions 1. ** Found [state 154] (consequent(i3)):Set/Sequent {} -- found required number of solutions 1. (true):Bool (0.000 sec for parse, 138815 rewrites(241.840 sec), 7398605 matches, 80054 memo hits)
TRANSITIVE'
#!python module TRANSITIVE' ( X :: TRIV, R :: RELATION(X), T :: TRANSITIVE(X,R), C :: COMPLEMENT(X,R) ) { signature { [ Transitive' < Transitive ] } axioms { vars X Y Z : Elt vars R : Transitive' 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 . } }
PARTIALORDER'
#!python module PARTIALORDER' ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), T :: TRANSITIVE(X,R), P :: PARTIALORDER(X,R,I,A,T), C :: COMPLEMENT(X,R), V :: TRANSITIVE'(X,R,T,C) ) { signature { [ PartialOrder' < Transitive' PartialOrder ] } }
OVERRIDE/REV2
#!python module OVERRIDE ( X :: TRIV, R :: RELATION(X), I :: IRREFLEXIVE(X,R), A :: ASYMMETRIC(X,R), T :: TRANSITIVE(X,R), P :: PARTIALORDER(X,R,I,A,T), C :: COMPLEMENT(X,R), V :: TRANSITIVE'(X,R,T,C), S :: PARTIALORDER'(X,R,I,A,T,P,C,V) ) { signature { op [_;_] : Relation Relation -> Relation op [_;_] : Irreflexive Irreflexive -> Irreflexive op [_;_] : Asymmetric Asymmetric -> Asymmetric op [_;_] : Transitive' Transitive -> Transitive op [_;_] : PartialOrder' PartialOrder -> PartialOrder } axioms { vars F G : Relation vars R : Asymmetric vars X Y : Elt eq deducible((X F Y) |- (X [F;G] Y)) = true . eq deducible((X G Y) |- ((Y F X),(X [F;G] Y))) = true . eq deducible((X [F;G] Y) |- ((X F Y),(X G Y))) = true . eq deducible((X [F;G] Y),(Y F X) |- (X F Y)) = true . eq deducible((X [R;G] Y) |- (X [R] Y)) = true . eq deducible((X [F;G] Y) |- (X F Y),((X G Y) /\ (X [F] Y))) = true . eq deducible((X G Y),(X [F] Y) |- (X [F;G] Y)) = true . } }
Updated