Nuprl Lemma : mk_lambdas_unroll

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


Proof




Definitions occuring in Statement :  mk_lambdas: mk_lambdas(F;m) nat_plus: + uall: [x:A]. B[x] top: Top 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: mk_lambdas(F;m) nat_plus: + top: Top all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A prop: bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b
Lemmas referenced :  primrec-unroll eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int nat_plus_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis isect_memberEquality voidElimination voidEquality because_Cache natural_numberEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination independent_pairFormation computeAll promote_hyp instantiate cumulativity independent_functionElimination sqequalAxiom

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



Date html generated: 2017_10_01-AM-08_40_06
Last ObjectModification: 2017_07_26-PM-04_27_53

Theory : untyped!computation


Home Index