Nuprl Lemma : mk_applies_lambdas_fun0

[F,G:Top]. ∀[m:ℕ].  (mk_applies(mk_lambdas_fun(F;m);G;m) x.mk_applies(x;G;m)))


Proof




Definitions occuring in Statement :  mk_applies: mk_applies(F;G;m) mk_lambdas_fun: mk_lambdas_fun(F;m) nat: uall: [x:A]. B[x] top: Top apply: a lambda: λx.A[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q 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] false: False implies:  Q not: ¬A top: Top prop: le: A ≤ B ge: i ≥  sq_type: SQType(T) guard: {T} mk_lambdas_fun: mk_lambdas_fun(F;m) mk_lambdas-fun: mk_lambdas-fun(F;G;n;m) uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q rev_implies:  Q bfalse: ff
Lemmas referenced :  assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_le_int eqtt_to_assert bool_subtype_base bool_wf bool_cases int_formula_prop_le_lemma intformle_wf le_wf not_wf bnot_wf assert_wf le_int_wf top_wf nat_wf int_term_value_subtract_lemma int_formula_prop_eq_lemma itermSubtract_wf intformeq_wf decidable__equal_int nat_properties int_subtype_base subtype_base_sq lelt_wf int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma itermConstant_wf itermAdd_wf itermVar_wf intformless_wf intformnot_wf satisfiable-full-omega-tt decidable__lt mk_applies_lambdas_fun
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename dependent_set_memberEquality independent_pairFormation hypothesis dependent_functionElimination addEquality natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll productElimination because_Cache instantiate equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom cumulativity lambdaFormation impliesFunctionality

Latex:
\mforall{}[F,G:Top].  \mforall{}[m:\mBbbN{}].    (mk\_applies(mk\_lambdas\_fun(F;m);G;m)  \msim{}  F  (\mlambda{}x.mk\_applies(x;G;m)))



Date html generated: 2016_05_15-PM-02_11_43
Last ObjectModification: 2016_01_15-PM-10_20_02

Theory : untyped!computation


Home Index