### Nuprl Lemma : p-fun-exp_wf

`∀[A:Type]. ∀[f:A ⟶ (A + Top)]. ∀[n:ℕ].  (f^n ∈ A ⟶ (A + Top))`

Proof

Definitions occuring in Statement :  p-fun-exp: `f^n` nat: `ℕ` uall: `∀[x:A]. B[x]` top: `Top` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  p-fun-exp: `f^n` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ`
Lemmas referenced :  primrec_wf top_wf p-id_wf p-compose_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesisEquality unionEquality hypothesis lambdaEquality natural_numberEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].  \mforall{}[n:\mBbbN{}].    (f\^{}n  \mmember{}  A  {}\mrightarrow{}  (A  +  Top))

Date html generated: 2016_05_15-PM-03_31_44
Last ObjectModification: 2015_12_27-PM-01_11_21

Theory : general

Home Index