BetweennessOuterTransitivityFlipped-2 Show Code edit
thm (BetweennessOuterTransitivityFlipped-2 ((A a) (B a) (C a) (D a)) ()
(→
(∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))))
# First, <code>C a ≡ C D ∧ between B C a</code>.
A B C D a BetweennessOuterTransitivityFlipped-bca
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))))
# Next, <code>between B C D</code>
(∧ (between A B C) (between B C D)) (¬ (= B C)) ConjunctionRightElimination
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∧ (between A B C) (between B C D)))
eliminateLeftConjunctInConsequent
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between B C D))
composeConjunction
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∧ (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))) (between B C D)))
a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D) ThereExistsConjunctionRightMovement
(↔ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))) (∧ (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))) (between B C D)))
eliminateBiconditionalForward
(→ (∧ (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))) (between B C D)) (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))))
applySyllogism
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))))
# Finally, <code>B ≠ C</code>
(∧ (between A B C) (between B C D)) (¬ (= B C)) ConjunctionLeftElimination
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (¬ (= B C)))
composeConjunction
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∧ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))) (¬ (= B C))))
a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ThereExistsConjunctionRightMovement
(↔ (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))) (∧ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))) (¬ (= B C))))
eliminateBiconditionalForward
(→ (∧ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))) (¬ (= B C))) (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))))
applySyllogism
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))))
)
edit