---

Step * 1 1 1 1 1 2 of Lemma urec-level-property


1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
5. n : ℤ
6. 0 < n
7. ∀x:urec(F). (urec-level(f;x) < n - 1 ⇒ (x ∈ F^urec-level(f;x) Void))
8. m : ℕ
9. x : F^m Void
10. ¬(m = 0 ∈ ℤ)
11. ∀m:ℕ. ((F^m Void) ⊆r Base)
12. z : F (F^m - 1 Void)
13. x = z ∈ (F (F^m - 1 Void))
14. con : Constr(T.F[T])
15. v1 : (F^m - 1 Void) List
16. [%18] : ap-con(con;v1) = z ∈ F[F^m - 1 Void]
17. (f z) = <con, v1> ∈ decomp{i:l}(T.F[T];F^m - 1 Void;z)
⊢ if null(v1) then 1 else imax-list(map(λt.urec-level(f;t);v1)) + 1 fi  < n
⇒ (con v1 ∈ F^if null(v1) then 1 else imax-list(map(λt.urec-level(f;t);v1)) + 1 fi  Void)
BY
{ TACTIC:(DVar `v1' THENA Auto) }

1
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
5. n : ℤ
6. 0 < n
7. ∀x:urec(F). (urec-level(f;x) < n - 1 ⇒ (x ∈ F^urec-level(f;x) Void))
8. m : ℕ
9. x : F^m Void
10. ¬(m = 0 ∈ ℤ)
11. ∀m:ℕ. ((F^m Void) ⊆r Base)
12. z : F (F^m - 1 Void)
13. x = z ∈ (F (F^m - 1 Void))
14. con : Constr(T.F[T])
15. [%18] : ap-con(con;[]) = z ∈ F[F^m - 1 Void]
16. (f z) = <con, []> ∈ decomp{i:l}(T.F[T];F^m - 1 Void;z)
⊢ if null([]) then 1 else imax-list(map(λt.urec-level(f;t);[])) + 1 fi  < n
⇒ (con [] ∈ F^if null([]) then 1 else imax-list(map(λt.urec-level(f;t);[])) + 1 fi  Void)

2
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : ⋂T:{T:Type| T ⊆r Base} . (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))
5. n : ℤ
6. 0 < n
7. ∀x:urec(F). (urec-level(f;x) < n - 1 ⇒ (x ∈ F^urec-level(f;x) Void))
8. m : ℕ
9. x : F^m Void
10. ¬(m = 0 ∈ ℤ)
11. ∀m:ℕ. ((F^m Void) ⊆r Base)
12. z : F (F^m - 1 Void)
13. x = z ∈ (F (F^m - 1 Void))
14. con : Constr(T.F[T])
15. u : F^m - 1 Void
16. v : (F^m - 1 Void) List
17. [%18] : ap-con(con;[u / v]) = z ∈ F[F^m - 1 Void]
18. (f z) = <con, [u / v]> ∈ decomp{i:l}(T.F[T];F^m - 1 Void;z)
⊢ if null([u / v]) then 1 else imax-list(map(λt.urec-level(f;t);[u / v])) + 1 fi  < n
⇒ (con [u / v] ∈ F^if null([u / v]) then 1 else imax-list(map(λt.urec-level(f;t);[u / v])) + 1 fi  Void)

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  (F[T]  \msubseteq{}r  Base))
4.  f  :  \mcap{}T:\{T:Type|  T  \msubseteq{}r  Base\}  .  (x:F[T]  {}\mrightarrow{}  decomp\{i:l\}(T.F[T];T;x))
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}x:urec(F).  (urec-level(f;x)  <  n  -  1  {}\mRightarrow{}  (x  \mmember{}  F\^{}urec-level(f;x)  Void))
8.  m  :  \mBbbN{}
9.  x  :  F\^{}m  Void
10.  \mneg{}(m  =  0)
11.  \mforall{}m:\mBbbN{}.  ((F\^{}m  Void)  \msubseteq{}r  Base)
12.  z  :  F  (F\^{}m  -  1  Void)
13.  x  =  z
14.  con  :  Constr(T.F[T])
15.  v1  :  (F\^{}m  -  1  Void)  List
16.  [\%18]  :  ap-con(con;v1)  =  z
17.  (f  z)  =  <con,  v1>
\mvdash{}  if  null(v1)  then  1  else  imax-list(map(\mlambda{}t.urec-level(f;t);v1))  +  1  fi    <  n
{}\mRightarrow{}  (con  v1  \mmember{}  F\^{}if  null(v1)  then  1  else  imax-list(map(\mlambda{}t.urec-level(f;t);v1))  +  1  fi    Void)


By

---

Latex:
TACTIC:(DVar  `v1'  THENA  Auto)

---

Home Index