---

Step * of Lemma l-ordered-single

∀[T:Type]. ∀x:T. ∀[R:T ⟶ T ⟶ ℙ]. l-ordered(T;x,y.R[x;y];[x])
BY
{ (Unfold `l-ordered` 0
   THEN Auto
   THEN (FLemma `l_before_member` [-1] THENA Auto)
   THEN (FLemma `l_before_member2` [-2] THENA Auto)
   THEN GenListD (-2)
   THEN GenListD (-1)
   THEN D (-2)
   THEN Try (Complete ((GenListD (-2) THEN Auto)))
   THEN D (-1)
   THEN Try (Complete ((GenListD (-1)⋅ THEN Auto)))
   THEN (InstLemma `l_before_antisymmetry` [⌜T⌝;⌜[x]⌝;⌜x⌝;⌜x⌝]⋅
         THENA (Auto
                THEN GenListD 0
                THEN Auto
                THEN Try (Complete ((GenListD 0 THEN Auto)))
                THEN D 0
                THEN Auto
                THEN GenListD (-1)
                THEN Auto)
         )
   THEN (HypSubst' (-3) (-4) THENA Auto)
   THEN (HypSubst' (-2) (-4) THENA Auto)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  l-ordered(T;x,y.R[x;y];[x])


By

---

Latex:
(Unfold  `l-ordered`  0
  THEN  Auto
  THEN  (FLemma  `l\_before\_member`  [-1]  THENA  Auto)
  THEN  (FLemma  `l\_before\_member2`  [-2]  THENA  Auto)
  THEN  GenListD  (-2)
  THEN  GenListD  (-1)
  THEN  D  (-2)
  THEN  Try  (Complete  ((GenListD  (-2)  THEN  Auto)))
  THEN  D  (-1)
  THEN  Try  (Complete  ((GenListD  (-1)\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `l\_before\_antisymmetry`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[x]\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  GenListD  0
                            THEN  Auto
                            THEN  Try  (Complete  ((GenListD  0  THEN  Auto)))
                            THEN  D  0
                            THEN  Auto
                            THEN  GenListD  (-1)
                            THEN  Auto)
              )
  THEN  (HypSubst'  (-3)  (-4)  THENA  Auto)
  THEN  (HypSubst'  (-2)  (-4)  THENA  Auto)
  THEN  Auto)

---

Home Index