---

Step * of Lemma ulinorder_lt_neg

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x,y:T.  Dec(R[x;y])) ⇒ UniformLinorder(T;x,y.R[x;y]) ⇒ (∀[a,b:T].  uiff(¬strict_part(x,y.R[x;y];a;b);R[b;a])))
BY
{ (((RepD THENA Auto) THEN ARepD ["compound";"basic"]) THEN Unfold `strict_part` 0) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. ∀[a:T]. R[a;a]
5. ∀[a,b,c:T].  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
6. ∀[x,y:T].  (x = y ∈ T) supposing (R[y;x] and R[x;y])
7. ∀x,y:T.  (R[x;y] ∨ R[y;x])
8. ∀[x,y:T].  R[x;y] supposing R[x;y]
9. [a] : T
10. [b] : T
⊢ uiff(¬(R[a;b] ∧ (¬R[b;a]));R[b;a])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:T.    Dec(R[x;y]))
    {}\mRightarrow{}  UniformLinorder(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mforall{}[a,b:T].    uiff(\mneg{}strict\_part(x,y.R[x;y];a;b);R[b;a])))


By

---

Latex:
(((RepD  THENA  Auto)  THEN  ARepD  ["compound";"basic"])  THEN  Unfold  `strict\_part`  0)

---

Home Index