---

Step * 1 1 1 1 2 2 1 of Lemma urec-level_wf


1. F : Type ⟶ Type
2. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
3. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
4. n : ℤ
5. 0 < n
6. ∀x:F^n - 1 Void. (urec-level(f;x) ∈ ℕ)
7. z : F (F^n - 1 Void)
8. ∀m:ℕ. ((F^m Void) ⊆r Base)
9. (f z) = (f z) ∈ decomp{i:l}(T.F[T];F^n - 1 Void;z)
10. T : {T:Type| T ⊆r Base} 
11. (F^n - 1 Void) = T ∈ {T:Type| T ⊆r Base} 
⊢ decomp{i:l}(T.F[T];T;z) ⊆r (con:Constr(T.F[T]) × {L:T List| ap-con(con;L) = z ∈ Base} )
BY
{ (Unfold `decomp` 0 THEN (D 0 THENA Auto) THEN D -1 THEN MemCD THEN Try (Trivial)) }

1
.....subterm..... T:t
2:n
1. F : Type ⟶ Type
2. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
3. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
4. n : ℤ
5. 0 < n
6. ∀x:F^n - 1 Void. (urec-level(f;x) ∈ ℕ)
7. z : F (F^n - 1 Void)
8. ∀m:ℕ. ((F^m Void) ⊆r Base)
9. (f z) = (f z) ∈ decomp{i:l}(T.F[T];F^n - 1 Void;z)
10. T : {T:Type| T ⊆r Base} 
11. (F^n - 1 Void) = T ∈ {T:Type| T ⊆r Base} 
12. con : Constr(T.F[T])
13. x1 : {L:T List| ap-con(con;L) = z ∈ F[T]} 
⊢ x1 ∈ {L:T List| ap-con(con;L) = z ∈ Base} 

2
.....eq aux..... 
1. F : Type ⟶ Type
2. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
3. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
4. n : ℤ
5. 0 < n
6. ∀x:F^n - 1 Void. (urec-level(f;x) ∈ ℕ)
7. z : F (F^n - 1 Void)
8. ∀m:ℕ. ((F^m Void) ⊆r Base)
9. (f z) = (f z) ∈ decomp{i:l}(T.F[T];F^n - 1 Void;z)
10. T : {T:Type| T ⊆r Base} 
11. (F^n - 1 Void) = T ∈ {T:Type| T ⊆r Base} 
12. con : Constr(T.F[T])
13. x1 : {L:T List| ap-con(con;L) = z ∈ F[T]} 
14. c1 : Constr(T.F[T])
⊢ istype({L:T List| ap-con(c1;L) = z ∈ Base} )

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  (F[T]  \msubseteq{}r  Base))
3.  f  :  \mcap{}T:\{T:Type|  T  \msubseteq{}r  Base\}  .  (x:F[T]  {}\mrightarrow{}  decomp\{i:l\}(T.F[T];T;x))
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mforall{}x:F\^{}n  -  1  Void.  (urec-level(f;x)  \mmember{}  \mBbbN{})
7.  z  :  F  (F\^{}n  -  1  Void)
8.  \mforall{}m:\mBbbN{}.  ((F\^{}m  Void)  \msubseteq{}r  Base)
9.  (f  z)  =  (f  z)
10.  T  :  \{T:Type|  T  \msubseteq{}r  Base\} 
11.  (F\^{}n  -  1  Void)  =  T
\mvdash{}  decomp\{i:l\}(T.F[T];T;z)  \msubseteq{}r  (con:Constr(T.F[T])  \mtimes{}  \{L:T  List|  ap-con(con;L)  =  z\}  )


By

---

Latex:
(Unfold  `decomp`  0  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  MemCD  THEN  Try  (Trivial))

---

Home Index