---

Step * of Lemma cw-pp-lemma

∀A:Type. ∀B:A ⟶ Type. ∀w:W(A;a.B[a]). ∀n:ℕ. ∀m:ℕn. ∀ss:ℕn ⟶ cw-step(A;a.B[a]).
  ((∀x:ℕn. (W-rel(A;a.B[a];w) x ss (ss x))) ⇒ (fst(snd((ss m))) ∈ W(A;a.B[a])))
BY
{ (Auto
   THEN Unfold `W` 0
   THEN (InstLemma `pcw-pp-lemma` [⌜Unit⌝;⌜λ2p.A⌝;⌜λ2p a.B[a]⌝;⌜so_lambda(p,a,b.⋅)⌝;⌜⋅⌝;⌜w⌝;⌜n⌝;⌜m⌝;⌜ss⌝]⋅
         THENA Auto
         )) }

1
1. A : Type
2. B : A ⟶ Type
3. w : W(A;a.B[a])
4. n : ℕ
5. m : ℕn
6. ss : ℕn ⟶ cw-step(A;a.B[a])
7. ∀x:ℕn. (W-rel(A;a.B[a];w) x ss (ss x))
8. x : ℕn
⊢ param-W-rel(Unit;p.A;p,a.B[a];p,a,b.⋅;⋅;w) x ss (ss x)

2
1. A : Type
2. B : A ⟶ Type
3. w : W(A;a.B[a])
4. n : ℕ
5. m : ℕn
6. ss : ℕn ⟶ cw-step(A;a.B[a])
7. ∀x:ℕn. (W-rel(A;a.B[a];w) x ss (ss x))
8. fst(snd((ss m))) ∈ pW (fst((ss m)))
⊢ fst(snd((ss m))) ∈ pW ⋅

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w:W(A;a.B[a]).  \mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.  \mforall{}ss:\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]).
    ((\mforall{}x:\mBbbN{}n.  (W-rel(A;a.B[a];w)  x  ss  (ss  x)))  {}\mRightarrow{}  (fst(snd((ss  m)))  \mmember{}  W(A;a.B[a])))


By

---

Latex:
(Auto
  THEN  Unfold  `W`  0
  THEN  (InstLemma  `pcw-pp-lemma`  [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.B[a]\mkleeneclose{};\mkleeneopen{}so\_lambda(p,a,b.\mcdot{})\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};
              \mkleeneopen{}ss\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index