### Nuprl Lemma : phi-star_wf

`∀[Phi:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ]. (Phi* ∈ ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ finite-nat-seq())`

Proof

Definitions occuring in Statement :  phi-star: `Phi*` finite-nat-seq: `finite-nat-seq()` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` phi-star: `Phi*` subtype_rel: `A ⊆r B`
Lemmas referenced :  nat_wf zero-seq_wf mk-finite-nat-seq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality hypothesis because_Cache functionEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[Phi:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}].  (Phi*  \mmember{}  ((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  finite-nat-seq())

Date html generated: 2016_05_14-PM-09_55_42
Last ObjectModification: 2016_01_15-AM-07_49_38

Theory : continuity

Home Index