---

Step * 1 of Lemma bnot-left-test


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])
BY
{ ((Assert ⌜xs[i] # xs[j]xs[k]⌝⋅ THENA EAuto 1) THEN BLemma `bnot-isleft` THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  xs  :  \{xs:Point  List|  geo-general-position(g;xs)\} 
3.  i  :  \mBbbN{}||xs||
4.  j  :  \{j:\mBbbN{}||xs|||  \mneg{}(i  =  j)\} 
5.  k  :  \{k:\mBbbN{}||xs|||  (\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j))\} 
\mvdash{}  \mneg{}\msubb{}isleft(xs[i];xs[j];xs[k])  =  isleft(xs[i];xs[k];xs[j])


By

---

Latex:
((Assert  \mkleeneopen{}xs[i]  \#  xs[j]xs[k]\mkleeneclose{}\mcdot{}  THENA  EAuto  1)  THEN  BLemma  `bnot-isleft`  THEN  Auto)

---

Home Index