---

Step * of Lemma l-ordered-inst

∀[T:Type]. ∀L:T List. ∀R:T ⟶ T ⟶ ℙ. ∀i:ℕ||L||. ∀j:ℕi.  (l-ordered(T;x,y.R[x;y];L) ⇒ R[L[j];L[i]])
BY
{ (Auto
   THEN Unfold `l-ordered` (-1)
   THEN BackThruSomeHyp
   THEN RepeatFor 2 (UnfoldTopAb 0)
   THEN Reduce 0
   THEN InstConcl [⌜λx.if (x =z 0) then j else i fi ⌝]⋅
   THEN Auto
   THEN Reduce 0
   THEN Try ((IntSegCases (-1) THEN Reduce 0 THEN Auto))
   THEN UnfoldTopAb 0
   THEN Reduce 0
   THEN Auto
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    (l-ordered(T;x,y.R[x;y];L)  {}\mRightarrow{}  R[L[j];L[i]])


By

---

Latex:
(Auto
  THEN  Unfold  `l-ordered`  (-1)
  THEN  BackThruSomeHyp
  THEN  RepeatFor  2  (UnfoldTopAb  0)
  THEN  Reduce  0
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}x.if  (x  =\msubz{}  0)  then  j  else  i  fi  \mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  ((IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto))
  THEN  UnfoldTopAb  0
  THEN  Reduce  0
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index