---

Step * of Lemma fix_wf-pcorec-partial-nat

∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[f:⋂X:P ⟶ Type
                                                          ((i:P ⟶ (X i) ⟶ partial(ℕ))
                                                          ⟶ i:P
                                                          ⟶ (ptuple(lbl,p.a[lbl;p];X) i)
                                                          ⟶ partial(ℕ))].
  (fix(f) ∈ i:P ⟶ (pcorec(lbl,p.a[lbl;p]) i) ⟶ partial(ℕ))
BY
{ (Unfold `pcorec` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[f:\mcap{}X:P  {}\mrightarrow{}  Type
                                                                                                                    ((i:P  {}\mrightarrow{}  (X  i)  {}\mrightarrow{}  partial(\mBbbN{}))
                                                                                                                    {}\mrightarrow{}  i:P
                                                                                                                    {}\mrightarrow{}  (ptuple(lbl,p.a[lbl;p];X)  i)
                                                                                                                    {}\mrightarrow{}  partial(\mBbbN{}))].
    (fix(f)  \mmember{}  i:P  {}\mrightarrow{}  (pcorec(lbl,p.a[lbl;p])  i)  {}\mrightarrow{}  partial(\mBbbN{}))


By

---

Latex:
(Unfold  `pcorec`  0  THEN  Auto)

---

Home Index