Nuprl Lemma : mk_lambdas_fun-unroll-first

[F:Top]. ∀[m:ℕ+].  (mk_lambdas_fun(F;m) ~ λx.mk_lambdas_fun(λg.(F f.(g (f x))));m 1))


Proof




Definitions occuring in Statement :  mk_lambdas_fun: mk_lambdas_fun(F;m) nat_plus: + uall: [x:A]. B[x] top: Top apply: a lambda: λx.A[x] subtract: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T mk_lambdas_fun: mk_lambdas_fun(F;m) top: Top int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: nat_plus: + all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] mk_applies: mk_applies(F;G;m) nat:
Lemmas referenced :  mk_lambdas-fun-shift-init int_term_value_subtract_lemma int_formula_prop_le_lemma itermSubtract_wf intformle_wf decidable__le subtract_wf le_wf top_wf nat_plus_wf primrec1_lemma primrec0_lemma lelt_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_plus_properties false_wf mk_lambdas-fun-unroll-first
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation hypothesis setElimination rename dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality computeAll sqequalAxiom because_Cache

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



Date html generated: 2016_05_15-PM-02_11_16
Last ObjectModification: 2016_01_15-PM-10_20_10

Theory : untyped!computation


Home Index