Nuprl Lemma : callbyvalueall_seq-lambdas-all

[L,G,H,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕ1].
  (callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.G[f]] H[g]);n;m) 
  callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.(g mk_lambdas(G[f];m))] H[g]);n;m))


Proof




Definitions occuring in Statement :  mk_applies: mk_applies(F;G;m) mk_lambdas: mk_lambdas(F;m) callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) int_seg: {i..j-} nat: uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a lambda: λx.A[x] add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  exists: x:A. B[x] member: t ∈ T nat: uall: [x:A]. B[x] int_seg: {i..j-} guard: {T} ge: i ≥  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) false: False implies:  Q not: ¬A top: Top prop: sq_type: SQType(T) callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b
Lemmas referenced :  subtract_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf itermAdd_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_term_value_add_lemma int_formula_prop_wf le_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma equal_wf subtype_base_sq int_subtype_base ge_wf less_than_wf int_seg_wf nat_wf top_wf add-zero le_int_wf bool_wf eqtt_to_assert assert_of_le_int mk_applies_lambdas2 eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot mk_applies_roll
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_pairFormation dependent_set_memberEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality natural_numberEquality addEquality productElimination dependent_functionElimination unionElimination independent_isectElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination intWeakElimination lambdaFormation sqequalAxiom isect_memberFormation equalityElimination promote_hyp

Latex:
\mforall{}[L,G,H,K,F:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[\mlambda{}f.G[f]]  H[g]);n;m) 
    \msim{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[\mlambda{}f.(g  mk\_lambdas(G[f];m))]  H[g]);n;m))



Date html generated: 2017_10_01-AM-08_42_25
Last ObjectModification: 2017_07_26-PM-04_29_11

Theory : untyped!computation


Home Index