---

Step * 1 of Lemma assert-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 ∈ ℤ))} 
⊢ ↑isleft(xs[i];xs[j];xs[k]) ⇐⇒ xs[i] leftof xs[j]xs[k]
BY
{ ((Assert ⌜xs[i] # xs[j]xs[k]⌝⋅ THENA EAuto 1)
   THEN InstLemma `assert-geo-isleft` [⌜g⌝;⌜xs[i]⌝;⌜xs[j]⌝;⌜xs[k]⌝]⋅
   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{}  \muparrow{}isleft(xs[i];xs[j];xs[k])  \mLeftarrow{}{}\mRightarrow{}  xs[i]  leftof  xs[j]xs[k]


By

---

Latex:
((Assert  \mkleeneopen{}xs[i]  \#  xs[j]xs[k]\mkleeneclose{}\mcdot{}  THENA  EAuto  1)
  THEN  InstLemma  `assert-geo-isleft`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}xs[i]\mkleeneclose{};\mkleeneopen{}xs[j]\mkleeneclose{};\mkleeneopen{}xs[k]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index