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 )