---

Step * 1 1 2 1 1 of Lemma in-hull-leftmost


1. g : OrientedPlane
2. u : Point
3. u1 : Point
4. u2 : Point
5. v : Point List
6. geo-general-position(g;[u; u1; [u2 / v]])
7. 2 < ||[u; u1; [u2 / v]]||
8. i : ℕ||[u; u1; [u2 / v]]||
9. j : ℕ||[u; u1; [u2 / v]]||
10. ¬(i = j ∈ ℤ)
11. ij ∈ Hull([u; u1; [u2 / v]])
12. hull-cmp(g;[u; u1; [u2 / v]];i;j) ∈ comparison({k:ℕ||[u; u1; [u2 / v]]||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
⊢ 0 < ||filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));upto(||[u; u1; [u2 / v]]||))||
BY
{ ((Reduce 0 THEN RepeatFor 3 ((RWO  "upto_decomp2" 0 THENA Auto)) THEN Reduce 0)
   THEN (GenConclTerm ⌜filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));
                              map(λi.(i + 1);map(λi.(i + 1);map(λi.(i + 1);upto((((||v|| + 1) + 1) + 1) - 1 - 1 
                                                                - 1)))))⌝⋅
         THENA Auto
         )
   ) }

1
1. g : OrientedPlane
2. u : Point
3. u1 : Point
4. u2 : Point
5. v : Point List
6. geo-general-position(g;[u; u1; [u2 / v]])
7. 2 < ||[u; u1; [u2 / v]]||
8. i : ℕ||[u; u1; [u2 / v]]||
9. j : ℕ||[u; u1; [u2 / v]]||
10. ¬(i = j ∈ ℤ)
11. ij ∈ Hull([u; u1; [u2 / v]])
12. hull-cmp(g;[u; u1; [u2 / v]];i;j) ∈ comparison({k:ℕ||[u; u1; [u2 / v]]||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} )
13. v1 : ℤ List
14. filter(λk.((¬b(k =z i)) ∧b (¬b(k =z j)));map(λi.(i + 1);map(λi.(i + 1);map(λi.(i + 1);upto((((||v|| + 1) + 1) + 1) 
                                                                               - 1 - 1 - 1)))))
= v1
∈ (ℤ List)
⊢ 0 < ||if (¬b(0 =z i)) ∧b (¬b(0 =z j))
          then [0 / 
                if (¬b(1 =z i)) ∧b (¬b(1 =z j)) then [1 / if (¬b(2 =z i)) ∧b (¬b(2 =z j)) then [2 / v1] else v1 fi ]
                if (¬b(2 =z i)) ∧b (¬b(2 =z j)) then [2 / v1]
                else v1
                fi ]
if (¬b(1 =z i)) ∧b (¬b(1 =z j)) then [1 / if (¬b(2 =z i)) ∧b (¬b(2 =z j)) then [2 / v1] else v1 fi ]
if (¬b(2 =z i)) ∧b (¬b(2 =z j)) then [2 / v1]
else v1
fi ||

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  u  :  Point
3.  u1  :  Point
4.  u2  :  Point
5.  v  :  Point  List
6.  geo-general-position(g;[u;  u1;  [u2  /  v]])
7.  2  <  ||[u;  u1;  [u2  /  v]]||
8.  i  :  \mBbbN{}||[u;  u1;  [u2  /  v]]||
9.  j  :  \mBbbN{}||[u;  u1;  [u2  /  v]]||
10.  \mneg{}(i  =  j)
11.  ij  \mmember{}  Hull([u;  u1;  [u2  /  v]])
12.  hull-cmp(g;[u;  u1;  [u2  /  v]];i;j)  \mmember{}  comparison(\{k:\mBbbN{}||[u;  u1;  [u2  /  v]]||| 
                                                                                                        (\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j))\}  )
\mvdash{}  0  <  ||filter(\mlambda{}k.((\mneg{}\msubb{}(k  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(k  =\msubz{}  j)));upto(||[u;  u1;  [u2  /  v]]||))||


By

---

Latex:
((Reduce  0  THEN  RepeatFor  3  ((RWO    "upto\_decomp2"  0  THENA  Auto))  THEN  Reduce  0)
  THEN  (GenConclTerm  \mkleeneopen{}filter(\mlambda{}k.((\mneg{}\msubb{}(k  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(k  =\msubz{}  j)));
                                                        map(\mlambda{}i.(i  +  1);map(\mlambda{}i.(i  +  1);map(\mlambda{}i.(i  +  1);upto((((||v||  +  1)  +  1)
                                                                                                                            +  1)  -  1  -  1  -  1)))))\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  )

---

Home Index