---

Step * 1 1 2 1 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 ∈ ℤ))} )
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 ||
BY
{ (BoolCase ⌜(0 =z i)⌝⋅ THENA Auto) }

---

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))\}  )
13.  v1  :  \mBbbZ{}  List
14.  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)))))
=  v1
\mvdash{}  0  <  ||if  (\mneg{}\msubb{}(0  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(0  =\msubz{}  j))
                    then  [0  / 
                                if  (\mneg{}\msubb{}(1  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(1  =\msubz{}  j))
                                    then  [1  /  if  (\mneg{}\msubb{}(2  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(2  =\msubz{}  j))  then  [2  /  v1]  else  v1  fi  ]
                                if  (\mneg{}\msubb{}(2  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(2  =\msubz{}  j))  then  [2  /  v1]
                                else  v1
                                fi  ]
if  (\mneg{}\msubb{}(1  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(1  =\msubz{}  j))  then  [1  /  if  (\mneg{}\msubb{}(2  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(2  =\msubz{}  j))  then  [2  /  v1]  else  v1  fi  ]
if  (\mneg{}\msubb{}(2  =\msubz{}  i))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(2  =\msubz{}  j))  then  [2  /  v1]
else  v1
fi  ||


By

---

Latex:
(BoolCase  \mkleeneopen{}(0  =\msubz{}  i)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index