---

Step * of Lemma l-ordered-decomp2

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].
  (∀[L:T List]
     (L = (filter(λy.R[y;x];L) @ [x / filter(λy.R[x;y];L)]) ∈ (T List)) supposing 
        (l-ordered(T;x,y.↑R[x;y];L) and 
        (x ∈ L))) supposing 
     (Trans(T;x,y.↑R[x;y]) and 
     Irrefl(T;x,y.↑R[x;y]) and 
     StAntiSym(T;x,y.↑R[x;y]))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN RW ListC 0
   THEN Try (Complete (Auto))
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN DProdsAndUnions
   THEN Try (Complete ((All(RepUR ``irrefl st_anti_sym``) THEN Assert ⌜False⌝⋅ THEN Auto)))) }

1
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)

2
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. v : T List
10. (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))
11. ↑R[u;x]
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 / filter(λy.R[x;y];v)])] ∈ (T List)

3
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)

---

Latex:

---

Latex:
No  Annotations
\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)  @  [x  /  filter(\mlambda{}y.R[x;y];L)]))  supposing 
                (l-ordered(T;x,y.\muparrow{}R[x;y];L)  and 
                (x  \mmember{}  L)))  supposing 
          (Trans(T;x,y.\muparrow{}R[x;y])  and 
          Irrefl(T;x,y.\muparrow{}R[x;y])  and 
          StAntiSym(T;x,y.\muparrow{}R[x;y]))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  RW  ListC  0
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  Try  (Complete  ((All(RepUR  ``irrefl  st\_anti\_sym``)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto))))

---

Home Index