Step * 1 1 1 1 1 of Lemma in-hull-transitivity


1. OrientedPlane
2. xs Point List
3. geo-general-position(g;xs)
4. : ℕ||xs||
5. : ℕ||xs||
6. : ℕ||xs||
7. (c i ∈ ℤ)) ∧ (c j ∈ ℤ))
8. ¬(i j ∈ ℤ)
9. ij ∈ Hull(xs)
10. : ℕ||xs||
11. (a i ∈ ℤ)) ∧ (a j ∈ ℤ))
12. : ℕ||xs||
13. (b i ∈ ℤ)) ∧ (b j ∈ ℤ))
14. ¬(c b ∈ ℤ)
15. ↑bc
16. ¬(b c ∈ ℤ)
17. ↑¬bbc
18. c ∈ ℤ
⊢ False
BY
(MoveToConcl (-4) THEN MoveToConcl (-2) THEN (GenConclTerm ⌜bc⌝⋅ THENA Auto) THEN All Thin THEN Auto) }


Latex:


Latex:

1.  g  :  OrientedPlane
2.  xs  :  Point  List
3.  geo-general-position(g;xs)
4.  i  :  \mBbbN{}||xs||
5.  j  :  \mBbbN{}||xs||
6.  c  :  \mBbbN{}||xs||
7.  (\mneg{}(c  =  i))  \mwedge{}  (\mneg{}(c  =  j))
8.  \mneg{}(i  =  j)
9.  ij  \mmember{}  Hull(xs)
10.  a  :  \mBbbN{}||xs||
11.  (\mneg{}(a  =  i))  \mwedge{}  (\mneg{}(a  =  j))
12.  b  :  \mBbbN{}||xs||
13.  (\mneg{}(b  =  i))  \mwedge{}  (\mneg{}(b  =  j))
14.  \mneg{}(c  =  b)
15.  \muparrow{}i  L  bc
16.  \mneg{}(b  =  c)
17.  \muparrow{}\mneg{}\msubb{}i  L  bc
18.  a  =  c
\mvdash{}  False


By


Latex:
(MoveToConcl  (-4)
  THEN  MoveToConcl  (-2)
  THEN  (GenConclTerm  \mkleeneopen{}i  L  bc\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)




Home Index