---

Step * of Lemma bnot-left-test

∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i:ℕ||xs||. ∀j:{j:ℕ||xs||| ¬(i = j ∈ ℤ)} .
∀k:{k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} .
  ¬bi L jk = i L kj
BY
{ ((UnivCD THENA Auto) THEN Unfold `left-test` 0) }

1
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. i : ℕ||xs||
4. j : {j:ℕ||xs||| ¬(i = j ∈ ℤ)} 
5. k : {k:ℕ||xs||| (¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))} 
⊢ ¬bisleft(xs[i];xs[j];xs[k]) = isleft(xs[i];xs[k];xs[j])

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}xs:\{xs:Point  List|  geo-general-position(g;xs)\}  .  \mforall{}i:\mBbbN{}||xs||.  \mforall{}j:\{j:\mBbbN{}||xs||| 
                                                                                                                                                                      \mneg{}(i  =  j)\}  .
\mforall{}k:\{k:\mBbbN{}||xs|||  (\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j))\}  .
    \mneg{}\msubb{}i  L  jk  =  i  L  kj


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `left-test`  0)

---

Home Index