Nuprl Lemma : mk_lambdas_fun_compose2

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


Proof




Definitions occuring in Statement :  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_compose1 false_wf le_wf primrec1_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,x.  (h  mk\_lambdas\_fun(f;n));m) 
    \msim{}  mk\_lambdas\_fun(\mlambda{}g.mk\_lambdas\_fun(\mlambda{}h,x.  (h  (f  g));m  -  n);n))



Date html generated: 2016_05_15-PM-02_11_33
Last ObjectModification: 2015_12_27-AM-00_34_38

Theory : untyped!computation


Home Index