Step
*
of Lemma
geo-out2-bet-out
∀e:BasicGeometry. ∀a,b,c,x,p:Point. (out(b ac)
⇒ out(b xp)
⇒ a_x_c
⇒ {out(b ap) ∧ out(b cp)})
BY
{ (Auto
THEN D -3
THEN D -2
THEN ExRepD
THEN RepeatFor 4 (((D 0 THENA Auto) THEN Try (Trivial)))
THEN ExRepD
THEN ∀h:hyp. (DNot h THEN DAnd 0 THEN (D 0 THENA Auto)) ) }
1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_x_p
15. b_a_c
⊢ False
2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_x_p
15. b_c_a
⊢ False
3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_p_x
15. b_a_c
⊢ False
4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_p_x
15. b_c_a
⊢ False
5
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_x_p
15. b_a_c
⊢ False
6
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_x_p
15. b_c_a
⊢ False
7
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_p_x
15. b_a_c
⊢ False
8
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_p_x
15. b_c_a
⊢ False
Latex:
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c,x,p:Point. (out(b ac) {}\mRightarrow{} out(b xp) {}\mRightarrow{} a\_x\_c {}\mRightarrow{} \{out(b ap) \mwedge{} out(b cp)\})
By
Latex:
(Auto
THEN D -3
THEN D -2
THEN ExRepD
THEN RepeatFor 4 (((D 0 THENA Auto) THEN Try (Trivial)))
THEN ExRepD
THEN \mforall{}h:hyp. (DNot h THEN DAnd 0 THEN (D 0 THENA Auto)) )
Home
Index