Nuprl Lemma : callbyvalueall_seq-fun4

[L,K,G,F,J,P,Q:Top]. ∀[n,m:ℕ]. ∀[p,q:ℤ].
  (callbyvalueall_seq(λi.K[if (i) < (p q)  then J[i;λout.if p=q  then P[i;out]  else Q[i]]  else L[i]];G;F;n;m) 
  callbyvalueall_seq(λi.K[if (i) < (p q)  then J[i;λout.Q[i]]  else L[i]];G;F;n;m))


Proof




Definitions occuring in Statement :  callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) nat: uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] less: if (a) < (b)  then c  else d int_eq: if a=b  then c  else d lambda: λx.A[x] subtract: m add: m int: 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 satisfiable_int_formula: satisfiable_int_formula(fmla) false: False implies:  Q not: ¬A 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 nequal: a ≠ b ∈ 
Lemmas referenced :  decidable__le subtract_wf nat_properties satisfiable-full-omega-tt 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 int_eq_as_ite less_as_ite lt_int_wf assert_of_lt_int eq_int_wf assert_of_eq_int neg_assert_of_eq_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 lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll addEquality productElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination intWeakElimination lambdaFormation sqequalAxiom equalityElimination promote_hyp isect_memberFormation

Latex:
\mforall{}[L,K,G,F,J,P,Q:Top].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[p,q:\mBbbZ{}].
    (callbyvalueall\_seq(\mlambda{}i.K[if  (i)  <  (p  +  q)
                                                            then  J[i;\mlambda{}out.if  i  -  p=q    then  P[i;out]    else  Q[i]]
                                                            else  L[i]];G;F;n;m)  \msim{}  callbyvalueall\_seq(\mlambda{}i.K[if  (i)  <  (p  +  q)
                                                                                                                                                              then  J[i;\mlambda{}out.Q[i]]
                                                                                                                                                              else  L[i]];G;F;n;m))



Date html generated: 2017_10_01-AM-08_42_15
Last ObjectModification: 2017_07_26-PM-04_29_05

Theory : untyped!computation


Home Index