---

Step * of Lemma l-ordered-decomp

∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].
  ∀[L:T List]. L = (filter(λy.R[y;x];L) @ filter(λy.(¬bR[y;x]);L)) ∈ (T List) supposing l-ordered(T;x,y.↑R[x;y];L) 
  supposing Trans(T;x,y.↑R[x;y])
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (RW ListC 0)
   THEN Try (Complete (Auto))
   THEN AutoSplit
   THEN Auto
   THEN ((InstLemma `filter_is_nil` [⌜T⌝;⌜λy.R[y;x]⌝;⌜v⌝]⋅ THENA (Auto THEN Reduce 0 THEN RWO "l_all_iff" 0 THEN Auto))
         THEN (HypSubst (-1) (-2) THEN HypSubst' -1 0)
         THEN All Reduce
         THEN EqCD
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
    \mforall{}[L:T  List]
        L  =  (filter(\mlambda{}y.R[y;x];L)  @  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;x]);L))  supposing  l-ordered(T;x,y.\muparrow{}R[x;y];L) 
    supposing  Trans(T;x,y.\muparrow{}R[x;y])


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (RW  ListC  0)
  THEN  Try  (Complete  (Auto))
  THEN  AutoSplit
  THEN  Auto
  THEN  ((InstLemma  `filter\_is\_nil`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}y.R[y;x]\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
                THENA  (Auto  THEN  Reduce  0  THEN  RWO  "l\_all\_iff"  0  THEN  Auto)
                )
              THEN  (HypSubst  (-1)  (-2)  THEN  HypSubst'  -1  0)
              THEN  All  Reduce
              THEN  EqCD
              THEN  Auto)\mcdot{})

---

Home Index