Nuprl Lemma : callbyvalueall-seq-extend0-2

∀[F,G,L:Top]. ∀[m:ℕ+].
  (callbyvalueall-seq(L;λx.x;mk_lambdas(λout.let x ⟵ F[out]
                                             in G[x];m - 1);0;m) ~ callbyvalueall-seq(λn.if (n =z m)
                                                                                         then mk_lambdas(λx.F[x];m - 1)
                                                                                         else L n
                                                                                         fi ;λx.x;mk_lambdas(λx.G[x];m)
                                                                                      ;0;m + 1))


Proof



Definitions occuring in Statement :  mk_lambdas: mk_lambdas(F;m),  callbyvalueall-seq: callbyvalueall-seq(L;G;F;n;m),  nat_plus: ℕ+,  callbyvalueall: callbyvalueall,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s],  apply: f a,  lambda: λx.A[x],  subtract: n - m,  add: n + m,  natural_number: $n,  sqequal: s ~ 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: P ⇒ Q,  prop: ℙ,  nat_plus: ℕ+,  all: ∀x:A. B[x],  decidable: Dec(P),  or: P ∨ Q,  uimplies: b 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_plus_wf,  primrec0_lemma,  lelt_wf,  int_formula_prop_wf,  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,  itermVar_wf,  itermAdd_wf,  itermConstant_wf,  intformless_wf,  intformnot_wf,  intformand_wf,  satisfiable-full-omega-tt,  decidable__lt,  nat_plus_properties,  false_wf,  callbyvalueall-seq-extend-2
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,G,L:Top].  \mforall{}[m:\mBbbN{}\msupplus{}].
    (callbyvalueall-seq(L;\mlambda{}x.x;mk\_lambdas(\mlambda{}out.let  x  \mleftarrow{}{}  F[out]
                                                                                          in  G[x];m  -  1);0;m) 
    \msim{}  callbyvalueall-seq(\mlambda{}n.if  (n  =\msubz{}  m)  then  mk\_lambdas(\mlambda{}x.F[x];m  -  1)  else  L  n  fi  ;\mlambda{}x.x
                                              ;mk\_lambdas(\mlambda{}x.G[x];m);0;m  +  1))


Date html generated: 2016_05_15-PM-02_13_00
Last ObjectModification: 2016_01_15-PM-10_19_09

Theory : untyped!computation


Home Index