List of theorems

List of theorems in general/Symmetric_point.gh:

(↔ (is-midpoint-of M A B) (∧ (between A M B) (≡ A M M B)))
(↔ (is-midpoint-of M A B) (is-midpoint-of M B A))
(↔ (between A B A) (= A B))
(→ (is-midpoint-of M A A) (= M A))
(is-midpoint-of A A A)
(∃ p′ (is-midpoint-of A P p′))
(→ (∧ (= P A) (∧ (is-midpoint-of A P P1) (is-midpoint-of A P P2))) (= P1 P2))
(→ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P P1) (is-midpoint-of A P P2))) (= P1 P2))
(→ (∧ (is-midpoint-of A P P1) (is-midpoint-of A P P2)) (= P1 P2))
(→ (∧ (is-midpoint-of A P1 P) (is-midpoint-of A P2 P)) (= P1 P2))
(→ (∧ (= P A) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (≡ P Q P′ Q′))
(∃ x (∃ x′ (∧ (∧ (between P′ P x) (≡ P x Q A)) (∧ (between x P′ x′) (≡ P′ x′ Q A)))))
(→ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∃ x (∃ x′ (∃ y (∃ y′ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P x) (≡ P x Q A)) (∧ (between x P′ x′) (≡ P′ x′ Q A))) (∧ (∧ (between Q′ Q y) (≡ Q y P A)) (∧ (between y Q′ y′) (≡ Q′ y′ P A))))))))))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between A P X))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between A Q Y))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between Q′ A Y))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between A Q′ Y′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between P′ A X))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between A P′ X′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ A X Y A))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ A Y′ X′ A))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ A Y A Y′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ A X A X′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (¬ (= X A)))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between X A X′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (between Y A Y′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ X A Y′ A))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ A X′ A Y))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ X′ Y′ Y X))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ Q X Q′ X′))
(→ (∧ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (∧ (∧ (∧ (between P′ P X) (≡ P X Q A)) (∧ (between X P′ X′) (≡ P′ X′ Q A))) (∧ (∧ (between Q′ Q Y) (≡ Q Y P A)) (∧ (between Y Q′ Y′) (≡ Q′ Y′ P A))))) (≡ P Q P′ Q′))
(→ (∧ (¬ (= P A)) (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q))) (≡ P Q P′ Q′))
(→ (∧ (is-midpoint-of A P′ P) (is-midpoint-of A Q′ Q)) (≡ P Q P′ Q′))
(→ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of A Q Q′)) (is-midpoint-of A R R′)) (≅ P Q R P′ Q′ R′))
(→ (∧ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of A Q Q′)) (is-midpoint-of A R R′)) (between P Q R)) (between P′ Q′ R′))
(→ (∧ (∧ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of A Q Q′)) (is-midpoint-of A R R′)) (is-midpoint-of A S S′)) (≡ P Q R S)) (≡ P′ Q′ R′ S′))
(→ (∧ (∧ (∧ (is-midpoint-of A P P′) (is-midpoint-of A Q Q′)) (is-midpoint-of A R R′)) (is-midpoint-of P Q R)) (is-midpoint-of P′ Q′ R′))