---

Step * 1 of Lemma r2-not-left-right-iff


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. (¬r2-left(a;b;c)) ⇒ (¬r2-left(a;c;b)) ⇒ (¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b)))
5. ¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b))
6. r2-left(a;b;c) ∨ r2-left(a;c;b)
⊢ False
BY
{ (Assert rv-pos-angle(2;a;b;c) BY
         (D -1
          THEN (FLemma `r2-left-pos-angle` [-1] THEN Auto)
          THEN RepeatFor 2 ((FLemma `rv-pos-angle-permute` [-1] THEN Auto))
          THEN BLemma `rv-pos-angle-symmetry`
          THEN Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. (¬r2-left(a;b;c)) ⇒ (¬r2-left(a;c;b)) ⇒ (¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b)))
5. ¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b))
6. r2-left(a;b;c) ∨ r2-left(a;c;b)
7. rv-pos-angle(2;a;b;c)
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  (\mneg{}r2-left(a;b;c))  {}\mRightarrow{}  (\mneg{}r2-left(a;c;b))  {}\mRightarrow{}  (\mneg{}((\mneg{}a\_b\_c)  \mwedge{}  (\mneg{}b\_c\_a)  \mwedge{}  (\mneg{}c\_a\_b)))
5.  \mneg{}((\mneg{}a\_b\_c)  \mwedge{}  (\mneg{}b\_c\_a)  \mwedge{}  (\mneg{}c\_a\_b))
6.  r2-left(a;b;c)  \mvee{}  r2-left(a;c;b)
\mvdash{}  False


By

---

Latex:
(Assert  rv-pos-angle(2;a;b;c)  BY
              (D  -1
                THEN  (FLemma  `r2-left-pos-angle`  [-1]  THEN  Auto)
                THEN  RepeatFor  2  ((FLemma  `rv-pos-angle-permute`  [-1]  THEN  Auto))
                THEN  BLemma  `rv-pos-angle-symmetry`
                THEN  Auto))

---

Home Index