Nuprl Lemma : mk_lambdas_fun_lambdas

[f:Top]. ∀[m:ℕ]. ∀[n:ℕ1].
  (mk_lambdas_fun(λh.(h mk_lambdas(f;n));m) mk_lambdas(mk_lambdas_fun(λg.(g f);m n);n))


Proof




Definitions occuring in Statement :  mk_lambdas: mk_lambdas(F;m) mk_lambdas_fun: mk_lambdas_fun(F;m) int_seg: {i..j-} nat: uall: [x:A]. B[x] top: Top apply: a lambda: λx.A[x] subtract: m add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: mk_lambdas: mk_lambdas(F;m) all: x:A. B[x] top: Top
Lemmas referenced :  mk_lambdas_fun_lambdas1 false_wf le_wf primrec0_lemma int_seg_wf nat_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation lambdaFormation hypothesis dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalAxiom addEquality setElimination rename because_Cache

Latex:
\mforall{}[f:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (mk\_lambdas\_fun(\mlambda{}h.(h  mk\_lambdas(f;n));m)  \msim{}  mk\_lambdas(mk\_lambdas\_fun(\mlambda{}g.(g  f);m  -  n);n))



Date html generated: 2016_05_15-PM-02_11_23
Last ObjectModification: 2015_12_27-AM-00_34_55

Theory : untyped!computation


Home Index