List of theorems

List of theorems in general/Out_lines.gh:

(↔ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∨ (between P A B) (between P B A))))
(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (between B P C)) (is-outside P A B))
(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (is-outside P A B)) (∨ (∧ (∧ (¬ (= A P)) (between A P C)) (between P A B)) (∧ (∧ (¬ (= A P)) (between A P C)) (between P B A))))
(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (is-outside P A B)) (between B P C))
(→ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (↔ (between B P C) (is-outside P A B)))
(→ (∧ (is-outside P A B) (∧ (¬ (= C P)) (between A P C))) (between B P C))
(∃ c (∧ (¬ (= c P)) (between A P c)))
(→ (is-outside P A B) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c))))
(→ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))))
(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))) (is-outside P A B))
(↔ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))))
(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (between P A B)) (¬ (between A P B)))
(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (between P B A)) (¬ (between A P B)))
(→ (is-outside P A B) (¬ (between A P B)))
(→ (is-outside P A B) (collinear A P B))
(→ (is-outside P A B) (∧ (collinear A P B) (¬ (between A P B))))
(→ (∧ (collinear A P B) (¬ (between A P B))) (∧ (¬ (= A P)) (¬ (= B P))))
(→ (∧ (collinear A P B) (¬ (between A P B))) (∨ (between P A B) (between P B A)))
(→ (∧ (collinear A P B) (¬ (between A P B))) (is-outside P A B))
(↔ (is-outside P A B) (∧ (collinear A P B) (¬ (between A P B))))
(→ (¬ (= A P)) (is-outside P A A))
(↔ (is-outside P A B) (is-outside P B A))
(→ (∧ (¬ (= B P)) (∧ (∨ (between P A B) (between P B A)) (∨ (between P B C) (between P C B)))) (∨ (between P A C) (between P C A)))
(→ (∧ (is-outside P A B) (is-outside P B C)) (is-outside P A C))
(→ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (∧ (∨ (between A R E) (between A E R)) (≡ A E B C))) (∧ (is-outside A E R) (≡ A E B C)))
(→ (∧ (¬ (= R A)) (¬ (= B C))) (∃ e (∧ (is-outside A e R) (≡ A e B C))))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (∨ (∨ (∧ (between A X R) (between A Y R)) (∧ (between A X R) (between A R Y))) (∨ (∧ (between A R X) (between A Y R)) (∧ (∧ (¬ (= A R)) (between A R X)) (between A R Y)))))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (∨ (between A X Y) (between A Y X)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (≡ A X A Y))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (= X Y))
(→ (∧ (is-outside P A B) (≤ P A P B)) (∃ y (∧ (is-outside P A B) (∧ (between P y B) (≡ P A P y)))))
(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (¬ (= P Y)))
(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (is-outside P Y B))
(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (= Y A))
(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (between P A B))
(→ (∧ (is-outside P A B) (≤ P A P B)) (between P A B))
(→ (between P A B) (≤ P A P B))
(→ (is-outside P A B) (↔ (≤ P A P B) (between P A B)))
(→ (∨ (between P S X) (between P X S)) (collinear X P S))
(→ (∧ (∧ (¬ (= P Q)) (collinear S P Q)) (collinear X P Q)) (collinear X P S))
(→ (∧ (∧ (¬ (= P Q)) (collinear P Q A)) (collinear P Q B)) (collinear P A B))
(→ (∧ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (collinear X P Q)) (collinear X P S))
(→ (∧ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (collinear X P S)) (collinear X P Q))
(→ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (↔ (collinear X P Q) (collinear X P S)))
(→ (∧ (∧ (¬ (= P Q)) (collinear P Q A)) (collinear P Q B)) (collinear Q A B))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear C P Q))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= A B)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (∧ (∧ (¬ (= A B)) (collinear A B P)) (collinear A B Q)))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear A P Q))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear B P Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q A))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A C Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q B))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A B Q))
(→ (∧ (= Q A) (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q)))) (collinear A B C))
(→ (∧ (¬ (= Q A)) (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q)))) (collinear A B C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A B C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (⊥))
(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (= P Q))
(∃ a (∃ b (∃ c (¬ (collinear a b c)))))
(→ (¬ (collinear A B P)) (∃ c (¬ (collinear A B c))))
(→ (∧ (= A X) (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (collinear A B Z))) (collinear X Y Z))
(→ (∧ (¬ (= A X)) (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (collinear A B Z))) (collinear X Y Z))
(→ (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (¬ (collinear X Y Z))) (¬ (collinear A B Z)))
(→ (∧ (∧ (collinear A B Y) (¬ (= A B))) (¬ (collinear X Y Z))) (∃ c (¬ (collinear A B c))))
(→ (∧ (¬ (= A B)) (¬ (collinear X Y Z))) (∃ c (¬ (collinear A B c))))
(→ (¬ (= A B)) (∃ c (¬ (collinear A B c))))
(→ (∧ (= A B) (∧ (∧ (∧ (between A B C) (between D B E)) (≡ A B D B)) (≡ B C B E))) (= D B))
(→ (∧ (= A B) (∧ (∧ (∧ (between A B C) (between D B E)) (≡ A B D B)) (≡ B C B E))) (≡ A E C D))
(→ (∧ (¬ (= A B)) (∧ (∧ (∧ (between A B C) (between D B E)) (≡ A B D B)) (≡ B C B E))) (≡ A E C D))
(→ (∧ (∧ (∧ (between A B C) (between D B E)) (≡ A B D B)) (≡ B C B E)) (≡ A E C D))