1. Toshimi Sawada Avatar Toshimi Sawada
  2. Untitled project
  3. CafeOBJ

Wiki

Clone wiki

CafeOBJ / OSEK / contents / index-e / 07_Override

View History

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