---

Step * 3 of Lemma l-ordered-decomp2


1. T : Type
2. R : T ⟶ T ⟶ 𝔹
3. x : T
4. StAntiSym(T;x,y.↑R[x;y])
5. Irrefl(T;x,y.↑R[x;y])
6. Trans(T;x,y.↑R[x;y])
7. u : T
8. ¬↑R[x;u]
9. ¬↑R[u;x]
10. v : T List
11. (v = (filter(λy.R[y;x];v) @ [x / filter(λy.R[x;y];v)]) ∈ (T List)) supposing 
       (l-ordered(T;x,y.↑R[x;y];v) and 
       (x ∈ v))
12. x = u ∈ T
13. l-ordered(T;x,y.↑R[x;y];v)
14. ∀y:T. ((y ∈ v) ⇒ (↑R[u;y]))
⊢ [u / v] = (filter(λy.R[y;x];v) @ [x / filter(λy.R[x;y];v)]) ∈ (T List)
BY
{ ((InstLemma `filter_is_nil` [⌜T⌝;⌜λy.R[y;x]⌝;⌜v⌝]⋅ THENA Auto)
   THEN Reduce 0
   THEN Try (Complete ((RWO "l_all_iff" 0 THEN Auto)))
   THEN HypSubst (-1) 0
   THEN HypSubst (-1) (-5)
   THEN AllReduce
   THEN (EqCD THEN Auto)
   THEN (RWO "filter_trivial" 0 THEN Auto)
   THEN RepUR ``so_apply`` 0
   THEN (RWO "l_all_iff" 0 THEN Auto)
   THEN (InstHyp [⌜x1⌝] (-4)⋅ THENA Auto)
   THEN (Subst ⌜R x x1 ~ R[x;x1]⌝ 0⋅ THENA (RepUR ``so_apply`` 0 THEN Auto))
   THEN All(RepUR ``st_anti_sym``)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  StAntiSym(T;x,y.\muparrow{}R[x;y])
5.  Irrefl(T;x,y.\muparrow{}R[x;y])
6.  Trans(T;x,y.\muparrow{}R[x;y])
7.  u  :  T
8.  \mneg{}\muparrow{}R[x;u]
9.  \mneg{}\muparrow{}R[u;x]
10.  v  :  T  List
11.  (v  =  (filter(\mlambda{}y.R[y;x];v)  @  [x  /  filter(\mlambda{}y.R[x;y];v)]))  supposing 
              (l-ordered(T;x,y.\muparrow{}R[x;y];v)  and 
              (x  \mmember{}  v))
12.  x  =  u
13.  l-ordered(T;x,y.\muparrow{}R[x;y];v)
14.  \mforall{}y:T.  ((y  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}R[u;y]))
\mvdash{}  [u  /  v]  =  (filter(\mlambda{}y.R[y;x];v)  @  [x  /  filter(\mlambda{}y.R[x;y];v)])


By

---

Latex:
((InstLemma  `filter\_is\_nil`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}y.R[y;x]\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Complete  ((RWO  "l\_all\_iff"  0  THEN  Auto)))
  THEN  HypSubst  (-1)  0
  THEN  HypSubst  (-1)  (-5)
  THEN  AllReduce
  THEN  (EqCD  THEN  Auto)
  THEN  (RWO  "filter\_trivial"  0  THEN  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  (RWO  "l\_all\_iff"  0  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}R  x  x1  \msim{}  R[x;x1]\mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``so\_apply``  0  THEN  Auto))
  THEN  All(RepUR  ``st\_anti\_sym``)
  THEN  Auto)

---

Home Index