---

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

.....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. con : ⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T])
10. v1 : {L:(F^n - 1 Void) List| (con L) = z ∈ Base} 
11. ¬(v1 = [] ∈ ((F^n - 1 Void) List))
12. (f z) = <con, v1> ∈ (con:⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T]) × {L:(F^n - 1 Void) List| (con L) = z ∈ Base} )
⊢ map(λt.urec-level(f;t);v1) ∈ {L:ℕ List| ¬(L = [] ∈ (ℤ List))} 
BY
{ TACTIC:MemTypeCD }

1
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. con : ⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T])
10. v1 : {L:(F^n - 1 Void) List| (con L) = z ∈ Base} 
11. ¬(v1 = [] ∈ ((F^n - 1 Void) List))
12. (f z) = <con, v1> ∈ (con:⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T]) × {L:(F^n - 1 Void) List| (con L) = z ∈ Base} )
⊢ map(λt.urec-level(f;t);v1) ∈ ℕ List

2
.....set predicate..... 
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. con : ⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T])
10. v1 : {L:(F^n - 1 Void) List| (con L) = z ∈ Base} 
11. ¬(v1 = [] ∈ ((F^n - 1 Void) List))
12. (f z) = <con, v1> ∈ (con:⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T]) × {L:(F^n - 1 Void) List| (con L) = z ∈ Base} )
⊢ ¬(map(λt.urec-level(f;t);v1) = [] ∈ (ℤ List))

3
.....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. con : ⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T])
10. v1 : {L:(F^n - 1 Void) List| (con L) = z ∈ Base} 
11. ¬(v1 = [] ∈ ((F^n - 1 Void) List))
12. (f z) = <con, v1> ∈ (con:⋂T:{T:Type| T ⊆r Base} . ((T List) ⟶ F[T]) × {L:(F^n - 1 Void) List| (con L) = z ∈ Base} )
13. L : ℕ List
⊢ istype(¬(L = [] ∈ (ℤ List)))

---

Latex:

---

Latex:
.....wf..... 
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.  con  :  \mcap{}T:\{T:Type|  T  \msubseteq{}r  Base\}  .  ((T  List)  {}\mrightarrow{}  F[T])
10.  v1  :  \{L:(F\^{}n  -  1  Void)  List|  (con  L)  =  z\} 
11.  \mneg{}(v1  =  [])
12.  (f  z)  =  <con,  v1>
\mvdash{}  map(\mlambda{}t.urec-level(f;t);v1)  \mmember{}  \{L:\mBbbN{}  List|  \mneg{}(L  =  [])\} 


By

---

Latex:
TACTIC:MemTypeCD

---

Home Index