List of theorems

List of theorems in general/Orthogonality.gh:

(↔ (is-right-angle A B C) (∃ c′ (∧ (is-midpoint-of B C c′) (≡ A C A c′))))
(→ antecedent (≡ A B C D)) , (→ antecedent (≡ C D E F))(→ antecedent (≡ A B E F))
(→ (∧ (∧ (is-midpoint-of B C C′) (≡ A C A C′)) (is-midpoint-of B A A′)) (∧ (is-midpoint-of B A A′) (≡ C A C A′)))
(→ (is-right-angle A B C) (is-right-angle C B A))
(↔ (is-right-angle A B C) (is-right-angle C B A))
(→ (∧ (∧ (is-right-angle A B C) (¬ (= A B))) (collinear B A A′)) (is-right-angle A′ B C))
(→ (∧ (∧ (is-midpoint-of B C C″) (≡ A C A C″)) (is-midpoint-of B C C′)) (= C″ C′))
(→ (∧ (is-right-angle A B C) (is-midpoint-of B C C′)) (is-right-angle A B C′))
(is-right-angle A B B)
(→ (∧ (∧ (∧ (is-midpoint-of B C C′) (≡ A C A C′)) (∧ (is-midpoint-of B C C″) (≡ A′ C A′ C″))) (between A C A′)) (= C′ C″))
(→ (∧ (∧ (∧ (is-midpoint-of B C C′) (≡ A C A C′)) (∧ (is-midpoint-of B C C″) (≡ A′ C A′ C″))) (between A C A′)) (≡ A′ C A′ C′))
(→ (∧ (∧ (∧ (is-midpoint-of B C C′) (≡ A C A C′)) (∧ (is-midpoint-of B C C″) (≡ A′ C A′ C″))) (between A C A′)) (= C C′))
(→ (∧ (∧ (∧ (is-midpoint-of B C C′) (≡ A C A C′)) (∧ (is-midpoint-of B C C″) (≡ A′ C A′ C″))) (between A C A′)) (= B C))
(→ (∧ (∧ (is-right-angle A B C) (is-right-angle A′ B C)) (between A C A′)) (= B C))
(→ (∧ (∧ (= A A′) (= B B′)) (= C C′)) (↔ (is-right-angle A B C) (is-right-angle A′ B′ C′)))
(→ (∧ (is-midpoint-of B C Z) (≡ A C A Z)) (is-right-angle A B C))
(→ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∃ c′ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C c′) (≡ A C A c′)))))
(→ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∃ a′ (∧ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∧ (is-midpoint-of C A a′) (≡ B A B a′)))))
(→ (∧ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∧ (is-midpoint-of C A A′) (≡ B A B A′))) (is-right-angle C′ C A))
(→ (∧ (∧ (is-midpoint-of C A Z) (≡ C′ A C′ Z)) (is-midpoint-of C A A′)) (= Z A′))
(→ (∧ (∧ (is-midpoint-of C A Z) (≡ C′ A C′ Z)) (is-midpoint-of C A A′)) (≡ C′ A C′ A′))
(→ (∧ (is-right-angle C′ C A) (is-midpoint-of C A A′)) (≡ C′ A C′ A′))
(→ (∧ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∧ (is-midpoint-of C A A′) (≡ B A B A′))) (≡ A′ C A′ C′))
(→ (∧ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∧ (is-midpoint-of C A A′) (≡ B A B A′))) (is-right-angle A′ B C))
(→ (∧ (∧ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (∧ (is-midpoint-of B C C′) (≡ A C A C′))) (∧ (is-midpoint-of C A A′) (≡ B A B A′))) (= B C))
(→ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (is-right-angle A C B))) (= B C))
(→ (∧ (is-right-angle A B C) (is-right-angle A C B)) (= B C))
(→ (is-right-angle A B A) (= A B))
(→ (∧ (is-right-angle A B C) (collinear A B C)) (∨ (= A B) (= C B)))
(→ (= B C) (is-right-angle A B C))
(→ (∧ (= B C) (∧ (is-right-angle A B C) (≅ A B C A′ B′ C′))) (is-right-angle A′ B′ C′))
(→ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (≅ A B C A′ B′ C′))) (∃ d (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C d) (≡ A C A d)) (≅ A B C A′ B′ C′)))))
(→ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (∃ d′ (∧ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (is-midpoint-of B′ C′ d′))))
(→ (∧ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (is-midpoint-of B′ C′ D′)) (¬ (= B′ C′)))
(→ antecedent (is-midpoint-of M A B))(→ antecedent (between A M B))
(→ (∧ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (is-midpoint-of B′ C′ D′)) (≡ D A D′ A′))
(→ (∧ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (is-midpoint-of B′ C′ D′)) (≡ A′ C′ A′ D′))
(→ (∧ (∧ (¬ (= B C)) (∧ (∧ (is-midpoint-of B C D) (≡ A C A D)) (≅ A B C A′ B′ C′))) (is-midpoint-of B′ C′ D′)) (is-right-angle A′ B′ C′))
(→ (∧ (¬ (= B C)) (∧ (is-right-angle A B C) (≅ A B C A′ B′ C′))) (is-right-angle A′ B′ C′))
(→ (∧ (is-right-angle A B C) (≅ A B C A′ B′ C′)) (is-right-angle A′ B′ C′))
(↔ (⟂at A B C D X) (∧ (∧ (∧ (∧ (¬ (= A B)) (¬ (= C D))) (collinear X A B)) (collinear X C D)) (∀ u (∀ v (→ (∧ (collinear u A B) (collinear v C D)) (is-right-angle u X v))))))
(↔ (⟂at A B C D X) (⟂at C D A B X))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X))) (collinear B U U0))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X))) (collinear B U X))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X))) (collinear B X U0))
(→ (∧ (= B U) (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X)))) (collinear X U U0))
(→ (∧ (¬ (= B U)) (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X)))) (collinear X U U0))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X))) (collinear X U U0))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B U0)) (collinear A B X)) (collinear A B U)) (is-right-angle U X V)) (¬ (= U X))) (is-right-angle U0 X V))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (¬ (= C D))) (collinear X A B)) (collinear X C D)) (∧ (∧ (∧ (∧ (collinear U A B) (collinear V C D)) (¬ (= U X))) (¬ (= V X))) (is-right-angle U X V))) (∧ (collinear U0 A B) (collinear V0 C D))) (is-right-angle U0 X V))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= A B)) (¬ (= C D))) (collinear X A B)) (collinear X C D)) (∧ (∧ (∧ (∧ (collinear U A B) (collinear V C D)) (¬ (= U X))) (¬ (= V X))) (is-right-angle U X V))) (∧ (collinear U0 A B) (collinear V0 C D))) (is-right-angle U0 X V0))
(→ (∧ (∧ (∧ (∧ (¬ (= A B)) (¬ (= C D))) (collinear X A B)) (collinear X C D)) (∃ u (∃ v (∧ (∧ (∧ (∧ (collinear u A B) (collinear v C D)) (¬ (= u X))) (¬ (= v X))) (is-right-angle u X v))))) (→ (∧ (collinear U0 A B) (collinear V0 C D)) (is-right-angle U0 X V0)))
(→ (∧ (∧ (∧ (∧ (¬ (= A B)) (¬ (= C D))) (collinear X A B)) (collinear X C D)) (∃ u (∃ v (∧ (∧ (∧ (∧ (collinear u A B) (collinear v C D)) (¬ (= u X))) (¬ (= v X))) (is-right-angle u X v))))) (⟂at A B C D X))
(→ (⟂at A B C D X) (is-right-angle A X C))
(→ (∧ (∧ (∧ (∧ (= A A′) (= B B′)) (= C C′)) (= D D′)) (= X X′)) (↔ (⟂at A B C D X) (⟂at A′ B′ C′ D′ X′)))
(↔ (⟂at A B C D X) (⟂at B A C D X))
(↔ (⟂at A B C D X) (⟂at A B D C X))
(↔ (⟂at A B C D X) (⟂at B A D C X))
(¬ (⟂at A B A B X))
(↔ (⟂ A B C D) (∃ x (⟂at A B C D x)))
(¬ (⟂ A B A B))
(→ (⟂at A B C D X) (⟂ A B C D))
(→ (∧ (∧ (⟂at A B C D X) (collinear Y A B)) (collinear Y C D)) (is-right-angle Y X Y))
(→ (∧ (∧ (⟂at A B C D X) (collinear Y A B)) (collinear Y C D)) (= X Y))
(→ (∧ (∧ (⟂at A B C D Y) (collinear X A B)) (collinear X C D)) (⟂at A B C D X))
(→ (∧ (∧ (⟂ A B C D) (collinear X A B)) (collinear X C D)) (⟂at A B C D X))
(→ (⟂at A B C D X0) (∧ (collinear X0 A B) (collinear X0 C D)))
(→ (∀ y (→ (∧ (collinear y A B) (collinear y C D)) (= X y))) (→ (∧ (collinear X0 A B) (collinear X0 C D)) (= X X0)))
(→ (∧ (⟂at A B C D X0) (∀ y (→ (∧ (collinear y A B) (collinear y C D)) (= X y)))) (= X X0))
(→ (∧ (⟂at A B C D X0) (∀ y (→ (∧ (collinear y A B) (collinear y C D)) (= X y)))) (⟂at A B C D X))
(→ (∧ (⟂ A B C D) (∀ y (→ (∧ (collinear y A B) (collinear y C D)) (= X y)))) (⟂at A B C D X))