List of theorems

List of theorems in general/Midpoint.gh:

(→ (∧ (∧ (= M M′) (= A A′)) (= B B′)) (↔ (is-midpoint-of M A B) (is-midpoint-of M′ A′ B′)))
(→ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (∃ b′ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B b′))))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B B′)) (≡ P B P′ B′))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B B′)) (≡ P′ B P B′))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B B′)) (= B B′))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B B′)) (is-midpoint-of A B B))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (is-midpoint-of A B B′)) (= A B))
(→ (∧ (is-midpoint-of A P P′) (is-midpoint-of B P P′)) (= A B))
(→ (between A M B) (→ (≡ M A M B) (∨ (= A B) (is-midpoint-of M A B))))
(→ (between M B A) (→ (≡ M A M B) (∨ (= A B) (is-midpoint-of M A B))))
(→ (between B A M) (→ (≡ M A M B) (∨ (= A B) (is-midpoint-of M A B))))
(→ (∧ (collinear A M B) (≡ M A M B)) (∨ (= A B) (is-midpoint-of M A B)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (∃ p′ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B p′))))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (collinear D B P′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (≡ P A P′ C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (≡ P C P′ A))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (≅ A P C C P′ A))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (= P P′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (is-midpoint-of P A C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (≅ B D P D B P′)) (is-midpoint-of P B D))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= B D))) (≡ A B C D)) (≡ B C D A)) (collinear A P C)) (collinear B P D)) (∧ (is-midpoint-of P A C) (is-midpoint-of P B D)))
(→ (∧ (∧ (collinear A B C) (≡ C A C B)) (= A B)) (∃ x (is-midpoint-of x A B)))
(→ (∧ (∧ (collinear A B C) (≡ C A C B)) (is-midpoint-of C A B)) (∃ x (is-midpoint-of x A B)))
(→ (∧ (collinear A B C) (≡ C A C B)) (∃ x (is-midpoint-of x A B)))
(→ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∃ p (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (between C A p) (¬ (= A p))))))
(→ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (between C A P) (¬ (= A P)))) (∃ q (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B q) (≡ B q A P))))))
(→ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∃ r (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A r Q) (between B r P)))))
(→ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∃ x (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A x B) (between R x C)))))
(→ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (≡ P B Q A))
(→ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∃ r′ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A r′ Q) (≅ B R P A r′ Q)))))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (∧ (∧ (∧ (between B R P) (between A R′ Q)) (≡ B P A Q)) (≡ R P R′ Q)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (≡ R A R′ B))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (≡ Q R P R′))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (≅ A R Q B R′ P))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (collinear B R′ P))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (¬ (= B P)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (¬ (= B Q)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (¬ (collinear A Q B)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (= R R′))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (≡ A R R B))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (¬ (= C R)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∧ (∧ (between C A P) (¬ (= A P))) (∧ (between C B Q) (≡ B Q A P)))) (∧ (between A R Q) (between B R P))) (∧ (between A X B) (between R X C))) (∧ (between A R′ Q) (≅ B R P A R′ Q))) (is-midpoint-of X A B))
(→ (∧ (¬ (collinear A B C)) (≡ C A C B)) (∃ x (is-midpoint-of x A B)))
(→ (≡ C A C B) (∃ x (is-midpoint-of x A B)))