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

Wiki

Clone wiki

CafeOBJ / OSEK / contents / index-e / backup / 07_Combination_of_Relations

View History

Combenation of Relations

In this section, we describe on combination of relation defined in the following module:

#!python
module COMBINE
(
  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 .
  }
}
Let F and G be arbitrary relations on Elt. Then a combination of F and G is represented as [F;G].

For all x,y : Elt, the value of (x [F;G] y) is defined as:

  • x [F;G] y is true if x F y is true.

  • x [F;G] y is equal to x G y if both of x F y and y F x are not true.

There are several properties satisfied by the combination of relations:

LEMMA1 on COMBINATION

Let F and G be arbitrary irreflexive relation. Then the combination [F;G] is also irreflexive

#!python
module CLAIM1/COMBINE
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMBINE(X,R))
  }
  signature
  {
    op  x : -> Elt
    ops f g : -> Irreflexive
    ops claim : -> Prop
  }
  axioms
  {
    eq claim = (x [f;g] x |- nil) .
  }
}
The proof score for verifying the above claim is:

#!python
open CLAIM1/COMBINE .
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
The result of execution of this score is: 
#!python
%CLAIM1/COMBINE(X, R, I)> *
-- reduce in %CLAIM1/COMBINE(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.140 sec), 4960 matches, 64 memo hits)
As the claim is reduced to be true, this lemma was proved.

LEMMA2 on COMBINATION

Let F and G be arbitrary asymmetric relations. Then, the combination [F;G] is also asymmetric.

#!python
module CLAIM2/COMBINE
(
  X :: TRIV,
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMBINE(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) .
  }
}
The proof score of this lemma is:

#!python
open CLAIM2/COMBINE .
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
This lemma2 holds because the claim is reduce to true in the execution of the above score.

#!python
%CLAIM2/COMBINE(X, R, A)> *
-- reduce in %CLAIM2/COMBINE(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.410 sec), 281375 matches, 3919 memo hits)

LEMMA3 on COMBINATION

Let F and G be arbitrary relation. Then if F is asymmetric, the sequent (x [F;G] y) |- (x [F] y) can be deducible for any x,y : Elt.

#!python
module CLAIM3/COMBINE
(
  X :: TRIV,
  R :: RELATION(X),
  A :: ASYMMETRIC(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMPLEMENT(X,R))
    pr(COMBINE(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)) .
  }
}
The proof score proving this claim is listed below: 
#!python
open CLAIM3/COMBINE .
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
The result of the execution of this score is: 
#!python
%CLAIM3/COMBINE(X, R, A)> *
-- reduce in %CLAIM3/COMBINE(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.130 sec), 8569 matches, 150 memo hits)
The claim is reduced to true, so this lemma holds.

LEMMA4 on COMBINATION

Let F and G be arbitrary relations on Elt. Then, the following sequents can be deduced.

  • (x [F;G] y) |- (x F y),((x G y)/(x [F] y)

  • (x G y),(x [F] y) |- (x [F;G] y)

#!python
module CLAIM4/COMBINE
(
  X :: TRIV,
  R :: RELATION(X),
  C :: COMPLEMENT(X,R)
)
{
  imports
  {
    pr(LK)
    pr(COMBINE(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)) .
  }
}
The following is the proof score for verification of claim1. 
#!python
open CLAIM4/COMBINE .
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
The claim1 is reduced to true in the execution of the above score. 
#!python
%CLAIM4/COMBINE(X, R, C)> *
-- reduce in %CLAIM4/COMBINE(X, R, C) : (claim1):Prop

** Found [state 34] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 1671 rewrites(0.310 sec), 54899 matches, 742 memo hits)
The proof score for verification of claim1 is listed below:

#!python
open CLAIM4/COMBINE .
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
The claim2 is also reduced to true. 
#!python
%CLAIM4/COMBINE(X, R, C)> *
-- reduce in %CLAIM4/COMBINE(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)

Gathering the lemma1, lemma2, lemma3 and lemma4, we obtain the following module redefining COMBINE. 

#!python
module COMBINE
(
  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 A : 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 [A;G] Y) |- (X [A] 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 .
  }
}

LEMMA5 on COMBINATION

Let F and G be arbitrary transitive relations. Suppose that F is a relation such that the following sequents are deducible for any x,y : Elt:

  • (x [F] y),(y F z) |- (x F z)

  • (x F y),(y [F] z) |- (x F z)

  • (x [F] y),(y [F] z) |- (x [F] z)

Then, the combination [F;G] is also transitive.

#!python
module CLAIM5/COMBINE
(
  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(COMBINE(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)) .
  }
}
The proof score for veryfing the claim becomes a little long:

#!python
open CLAIM5/COMBINE .
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
However, the claim is proved because it is reduced to true in the execution of the abave score.

#!python
%CLAIM5/COMBINE(X, R, I, A, T, C)> *
-- reduce in %CLAIM5/COMBINE(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(232.690 sec), 7398605 matches, 80054 memo hits)

We can declare a subset of the set of transitive relations whose elements satisfy the conditions listed in the above lemma5.

#!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 .
  }
}
Also, a subset of the set of partial orders can be declared: 
#!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 ]
  }
}
Then, we obtain the final version of the module COMBINE: 
#!python
module COMBINE
(
  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 X Y : Elt
    vars A : Asymmetric
    vars T : Transitive
    vars R : Transitive'
    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 [A;G] Y) |- (X [A] 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