---

Step * of Lemma howard-bar-rec_wf

∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ. ∀bar:∀s:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;s]). ∀mon:∀n:ℕ. ∀m:ℕn. ∀s:ℕn ⟶ ℕ.  (B[m;s] ⇒ B[n;s]).
∀base:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]). ∀ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]).
  ⇃(Q[0;seq-normalize(0;⊥)])
BY
{ (UnivCD THENA Auto) }

1
1. B : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ@i'
2. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ@i'
3. bar : ∀s:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;s])@i
4. mon : ∀n:ℕ. ∀m:ℕn. ∀s:ℕn ⟶ ℕ.  (B[m;s] ⇒ B[n;s])@i
5. base : ∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s])@i
6. ind : ∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s])@i
⊢ ⇃(Q[0;seq-normalize(0;⊥)])

---

Latex:

---

Latex:
\mforall{}B,Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}bar:\mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  B[n;s]).  \mforall{}mon:\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
                                                                                                                                        (B[m;s]  {}\mRightarrow{}  B[n;s]).
\mforall{}base:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    (B[n;s]  {}\mRightarrow{}  Q[n;s]).  \mforall{}ind:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
                                                                                                        ((\mforall{}m:\mBbbN{}.  Q[n  +  1;s.m@n])  {}\mRightarrow{}  Q[n;s]).
    \00D9(Q[0;seq-normalize(0;\mbot{})])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index