Prover9 Examples: Ternary Relations in Lattices
These theorems are based on the following paper.
-
R. Padmanabhan, "On Some Ternary Relations in Lattices",
Colloquium Mathematicum 15:195-198, 1966.
This work is part of an ongoing project of Padmanabhan, Veroff, and McCune.
A implies B.
prover9 -f head.in ab.in > ab.out ; ### ( ab.out.xml )
B implies C.
prover9 -f head.in bc.in > bc.out ; ### ( bc.out.xml )
B implies CS.
prover9 -f head.in bcs.in > bcs.out ; ### ( bcs.out.xml )
C implies D.
prover9 -f head.in cd.in > cd.out ; ### ( cd.out.xml )
CS implies D.
prover9 -f head.in csd.in > csd.out ; ### ( csd.out.xml )
Theorem 2, 1 implies 2.
prover9 -f head.in t2_12.in > t2_12.out ; ### ( t2_12.out.xml )
Theorem 2, 2 implies 3.
prover9 -f head.in t2_23.in > t2_23.out ; ### ( t2_23.out.xml )
Theorem 3, 1 implies 2.
prover9 -f head.in t3_12.in > t3_12.out ; ### ( t3_12.out.xml )
Theorem 4, 1 implies 2.
prover9 -f head.in t4_12.in > t4_12.out ; ### ( t4_12.out.xml )