---

Step * of Lemma W-measure-induction

∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[measure:T ⟶ W(A;a.B[a])]. ∀[P:T ⟶ ℙ].
  ((∀i:T. ((∀j:{j:T| measure[j] <  measure[i]} . P[j]) ⇒ P[i])) ⇒ (∀i:T. P[i]))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN UseWitness ⌜λg.fix((λf,x. (g x f)))⌝
   THEN (MemCD THENA Auto)
   THEN RW (AddrC [2] UnrollRecursionC) 0
   THEN Reduce 0
   THEN (MemCD THENA Auto)
   THEN Assert ⌜∀m:W(A;a.B[a]). ∀x:T.  ((measure[x] ≤  m) ⇒ (g x fix((λf,x. (g x f))) ∈ P[x]))⌝⋅) }

1
.....assertion..... 
1. T : Type
2. A : Type
3. B : A ⟶ Type
4. measure : T ⟶ W(A;a.B[a])
5. P : T ⟶ ℙ
6. g : ∀i:T. ((∀j:{j:T| measure[j] <  measure[i]} . P[j]) ⇒ P[i])
7. x : T
⊢ ∀m:W(A;a.B[a]). ∀x:T.  ((measure[x] ≤  m) ⇒ (g x fix((λf,x. (g x f))) ∈ P[x]))

2
1. T : Type
2. A : Type
3. B : A ⟶ Type
4. measure : T ⟶ W(A;a.B[a])
5. P : T ⟶ ℙ
6. g : ∀i:T. ((∀j:{j:T| measure[j] <  measure[i]} . P[j]) ⇒ P[i])
7. x : T
8. ∀m:W(A;a.B[a]). ∀x:T.  ((measure[x] ≤  m) ⇒ (g x fix((λf,x. (g x f))) ∈ P[x]))
⊢ g x fix((λf,x. (g x f))) ∈ P[x]

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[measure:T  {}\mrightarrow{}  W(A;a.B[a])].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}i:T.  ((\mforall{}j:\{j:T|  measure[j]  <    measure[i]\}  .  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:T.  P[i]))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  UseWitness  \mkleeneopen{}\mlambda{}g.fix((\mlambda{}f,x.  (g  x  f)))\mkleeneclose{}
  THEN  (MemCD  THENA  Auto)
  THEN  RW  (AddrC  [2]  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  (MemCD  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}m:W(A;a.B[a]).  \mforall{}x:T.    ((measure[x]  \mleq{}    m)  {}\mRightarrow{}  (g  x  fix((\mlambda{}f,x.  (g  x  f)))  \mmember{}  P[x]))\mkleeneclose{}\mcdot{})

---

Home Index