Nuprl Lemma : callbyvalueall_seq-fun2

[L,K,G,F:Top]. ∀[n,m:ℕ].
  (callbyvalueall_seq(λi.if i <then else K[i] fi ;G;F;n;m) callbyvalueall_seq(L;G;F;n;m))


Proof




Definitions occuring in Statement :  callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) nat: ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a lambda: λx.A[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q exists: x:A. B[x] uall: [x:A]. B[x] ge: i ≥  uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top and: P ∧ Q prop: sq_type: SQType(T) guard: {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 :  decidable__le subtract_wf nat_properties full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_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_wf le_wf decidable__equal_int intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma equal_wf subtype_base_sq int_subtype_base intformless_wf int_formula_prop_less_lemma ge_wf less_than_wf nat_wf le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot lt_int_wf assert_of_lt_int top_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis unionElimination dependent_pairFormation dependent_set_memberEquality isectElimination because_Cache natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation addEquality productElimination instantiate cumulativity equalityTransitivity equalitySymmetry intWeakElimination lambdaFormation sqequalAxiom equalityElimination promote_hyp isect_memberFormation

Latex:
\mforall{}[L,K,G,F:Top].  \mforall{}[n,m:\mBbbN{}].
    (callbyvalueall\_seq(\mlambda{}i.if  i  <z  m  then  L  i  else  K[i]  fi  ;G;F;n;m)  \msim{}  callbyvalueall\_seq(L;G;F;n;m))



Date html generated: 2018_05_21-PM-06_23_04
Last ObjectModification: 2018_05_19-PM-05_31_00

Theory : untyped!computation


Home Index