Nuprl Lemma : mk_lambdas-fun-unroll-first

[F,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm].
  (mk_lambdas-fun(F;λf.mk_applies(f;K;n);n;m) ~ λx.mk_lambdas-fun(F;λf.(mk_applies(f;K;n) x);n;m 1))


Proof




Definitions occuring in Statement :  mk_applies: mk_applies(F;G;m) mk_lambdas-fun: mk_lambdas-fun(F;G;n;m) int_seg: {i..j-} 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 nat_plus: + int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q exists: x:A. B[x] nat: all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False implies:  Q not: ¬A top: Top prop: subtype_rel: A ⊆B sq_type: SQType(T) guard: {T} ge: i ≥  less_than: a < b squash: T less_than': less_than'(a;b) mk_lambdas-fun: mk_lambdas-fun(F;G;n;m) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b le: A ≤ B iff: ⇐⇒ Q rev_implies:  Q subtract: m true: True
Lemmas referenced :  nat_plus_properties int_seg_properties decidable__le subtract_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf decidable__equal_int intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma equal-wf-base-T int_subtype_base subtype_base_sq nat_properties decidable__lt ge_wf less_than_wf int_seg_wf nat_plus_wf top_wf add-subtract-cancel le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot mk_applies_unroll false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel eq_int_wf mk_applies_fun lelt_wf assert_wf bnot_wf not_wf equal-wf-base bool_cases assert_of_eq_int iff_transitivity iff_weakening_uiff assert_of_bnot
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis setElimination rename natural_numberEquality productElimination dependent_pairFormation dependent_set_memberEquality because_Cache dependent_functionElimination unionElimination independent_isectElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll applyEquality addEquality instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination intWeakElimination lambdaFormation sqequalAxiom imageElimination isect_memberFormation equalityElimination promote_hyp minusEquality baseApply closedConclusion baseClosed impliesFunctionality

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



Date html generated: 2017_10_01-AM-08_40_41
Last ObjectModification: 2017_07_26-PM-04_28_13

Theory : untyped!computation


Home Index