Nuprl Lemma : callbyvalueall_seq-combine3-0

[F,L1,L2:Top]. ∀[m1,m2:ℕ].
  (callbyvalueall_seq(L1;λx.x;λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);0;m1) 
  callbyvalueall_seq(λi.if i <m1 then L1 else mk_lambdas_fun(λg.(L2[g] (i m1));m1) fi x.x
                      g.(F[partial_ap(g;m1 m2;m1)] partial_ap_gen(g;m1 m2;m1;m2));0;m1 m2))


Proof




Definitions occuring in Statement :  partial_ap: partial_ap(g;n;m) partial_ap_gen: partial_ap_gen(g;n;s;m) mk_lambdas_fun: mk_lambdas_fun(F;m) 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] subtract: m add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T top: Top int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: nat: ge: i ≥  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] mk_applies: mk_applies(F;G;m)
Lemmas referenced :  top_wf nat_wf primrec0_lemma lelt_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermVar_wf itermAdd_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_properties false_wf callbyvalueall_seq-combine3
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation sqequalRule lambdaFormation hypothesis setElimination rename dependent_functionElimination addEquality unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality computeAll because_Cache isect_memberFormation introduction sqequalAxiom

Latex:
\mforall{}[F,L1,L2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (callbyvalueall\_seq(L1;\mlambda{}x.x;\mlambda{}g.callbyvalueall\_seq(L2[g];\mlambda{}x.x;F[g];0;m2);0;m1) 
    \msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  m1  then  L1  i  else  mk\_lambdas\_fun(\mlambda{}g.(L2[g]  (i  -  m1));m1)  fi  ;\mlambda{}x.x
                                            ;\mlambda{}g.(F[partial\_ap(g;m1  +  m2;m1)]  partial\_ap\_gen(g;m1  +  m2;m1;m2));0;m1  +  m2))



Date html generated: 2016_05_15-PM-02_14_36
Last ObjectModification: 2016_01_15-PM-10_17_52

Theory : untyped!computation


Home Index