---

Step * 1 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. v : T List
9. (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))
10. ↑R[u;x]
11. ↑R[x;u]
12. (x ∈ v)
13. l-ordered(T;x,y.↑R[x;y];v)
14. ∀y:T. ((y ∈ v) ⇒ (↑R[u;y]))
⊢ [u / v] = [u / (filter(λy.R[y;x];v) @ [x; [u / filter(λy.R[x;y];v)]])] ∈ (T List)
BY
{ (All(RepUR ``irrefl st_anti_sym``) THEN (Assert ⌜False⌝ BY Auto) THEN InstHyp [⌜u⌝;⌜x⌝] 4⋅ 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.  v  :  T  List
9.  (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))
10.  \muparrow{}R[u;x]
11.  \muparrow{}R[x;u]
12.  (x  \mmember{}  v)
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]  =  [u  /  (filter(\mlambda{}y.R[y;x];v)  @  [x;  [u  /  filter(\mlambda{}y.R[x;y];v)]])]


By

---

Latex:
(All(RepUR  ``irrefl  st\_anti\_sym``)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}  BY
                          Auto)
  THEN  InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index