Wiki

Several Properties on Relation

In this section, we prove several properties on relation.

LEMMA1 on TOTALORDER

Let R be an arbitrary total order on Elt. Then for all x,y,z : Elt, the sequent ((x R y) |- (x R z),(z R y)) is deducible.

#!python
module CLAIM1/TOTALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T),
  O :: TOTALORDER(X,R,I,A,T,P)
)
{
  imports
  {
    pr(LEMMA1/LK)
    pr(PROVABLE)
  }
  signature
  {
    op r : -> TotalOrder
    ops x y z : -> Elt
    op claim : -> Prop
  }
  axioms
  {
    eq claim = deducible((x r y) |- (x r z),(z r y)) .
  }
}

This claim can be proved with the execution of the following proof score.

#!python
open CLAIM1/TOTALORDER .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (y r z),(y = z),(z r y)) .
eq q2 = ((x r y),(y r z) |- (x r z)) .
eq q3 = ((x r y),(y = z) |- (x r z)) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2,q3) .
eq ((x r y) |- (x r z),(z r y)) = consequent(i) .
red claim .
close

The following is the result of the execution of this proof score.

#!python
%CLAIM1/TOTALORDER(X, R, I, A, T, P, O)> *
-- reduce in %CLAIM1/TOTALORDER(X, R, I, A, T, P, O) : 
    (claim):Prop

** Found [state 40] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3157 rewrites(0.600 sec), 122748 matches, 1280 memo hits)

We obtain the CafeOBJ module which declares the above lemma.

#!python
module LEMMA1/TOTALORDER
(
  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(LK)
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : TotalOrder
    eq deducible((Y R Z) |- (Y R X),(X R Z)) = true .
    eq deducible((neg Y R X),(Y R Z) |- (X R Z)) = true .
  }
}

EXTEND

The module EXTEND extends a binary relation on Elt to that on Set.

#!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

Let R be an arbitrary binary relation on Elt. For any X,Y : Elt, the expression X [R] Y is equivalent to ¬(Y R X) The other module COMPLEMENT enables us to abbreviate a proposition ¬(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 on COMPLEMENT

Let R be an arbitrary irreflexive relation on Elt. Then, the complement of R [R] is reflexive.

#!python
module CLAIM1/COMPLEMENT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  C :: COMPLEMENT(X,R)
)
{
    imports
  {
    pr(LK)
  }
  signature
  {
    op r : -> Irreflexive
    op x : -> Elt
    op claim : -> Prop
  }
  axioms
  {
    eq claim = deducible(nil |- (x [r] x)) .
  }
}

The lemma1 can be proved by executing the following proof score.

#!python
open CLAIM1/COMPLEMENT .
ops q1 q2 : -> Sequent .
-- definition of completion
eq q1 = (nil |- (x [r] x),(x r x)) .
-- irreflexivity of partialorder
eq q2 = ((x r x) |- nil) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2) .
eq (nil |- (x [r] x)) = consequent(i) .
red claim .
close

Indeed, the claim of this lemma is reduced to be true.

#!python
-- opening module CLAIM1/COMPLEMENT(X, S, R, I, C).. done.
%CLAIM1/COMPLEMENT(X, S, R, I, C)> ...
-- reduce in %CLAIM1/COMPLEMENT(X, S, R, I, C) : (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.020 sec), 217 matches, 1 memo hits)

The lemma1 can be expressed as a CafeOBJ module.

#!python
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 on COMPLEMENT

Let R be an arbitrary asymmetric relation on Elt. Then, for all x : Elt and s : Set, the sequent (nil |- (x [r] s),(s [r] x)) is deducible.

#!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))) .
  }
}

This claim can be proved to be true with structural induction on S

#!python
-- [base case]
open CLAIM2/COMPLEMENT .
red claim(nil) .
close

The claim of the base case is obviously true.

#!python
%CLAIM2/COMPLEMENT(X, S, R, A)> 
-- 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)

The proof of the induction step is a little complicated:

#!python
-- [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 completion 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

The claim is reduced to true in the execution of the above score.

#!python
%CLAIM2/COMPLEMENT(X, S, R, A)> %CLAIM2/COMPLEMENT(X, S, R, A)> *
-- 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.170 sec), 1786294 matches, 18344 memo hits)

We obtain the module describing this lemma2.

#!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 on COMPLEMENT

Let R be an arbitrary transitive relation on Elt. Then, for all x,y : Elt and s : Set, the sequent ((x R y),(y [R] s) |- (x [R] s)) is deducible.

#!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)) .
  }
}

This lemma also can be proved with structural induction on S.

#!python
-- [base case]
open CLAIM3/COMPLEMENT .
red claim(nil) .
close

If S is empty, claim of the lemma3 is trivially true.

#!python
%CLAIM3/COMPLEMENT(X, S, R, T)> 
-- 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)

The proof score for induction step of the lemma3 is:

#!python
-- [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 completion
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

Executing the above score returns that the claim is reduced to true.

#!python
%CLAIM3/COMPLEMENT(X, S, R, T)> *
-- 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(11.780 sec), 1304434 matches, 12495 memo hits)

This results enables us to describe the module declaring the lemma3:

#!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 on COMPLEMENT

Let R be an arbitrary asymmetric relation on Elt. Then, for all x,y : Elt, if (x [r] y) holds if (x r y) is satisried.

#!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)) .
  }
}

The proof score for proof of this lemma is as follows:

#!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

The following is the result of the execution of this score.

#!python
%CLAIM4/COMPLEMENT(X, R, A)> *
-- 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)

We can describe the lemma as the following module.

#!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 .
  }
}

As a corollary of the lemma1 on total order, We can deduce the following lemma, concerning on the transitivity of complement of total order .

LEMMA5 on COMPLEMENT

Let R be an arbitrary total order. Then for all x,y,z : Elt,

(1) x [R] y, y r z |- x r z
(2) x r y, y [R] z |- x r z
(3) 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)) .
  }
}

The proof scores of these three claims and thier execution results are listed below:

The proof score for claim1

#!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

The result of execution of the above score:

#!python
%CLAIM5/COMPLEMENT(X, R, I, A, V, P, T)> *
-- 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)

The proof score for claim2

#!python
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

The result of execution of the above score:

#!python
%CLAIM5/COMPLEMENT(X, R, I, A, V, P, T)> *
-- 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)

The proof score for claim3

#!python
open CLAIM5/COMPLEMENT .
ops q1 q2 q3 q4 q5 q6 : -> 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

The result of execution of the above score:

#!python
%CLAIM5/COMPLEMENT(X, R, I, A, V, P, T)> *
-- 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(43.860 sec), 2301887 matches, 30145 memo hits)

We obtain the module declares the lemma5.

#!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  .
  }
}