Nuprl Lemma : callbyvalueall-seq-extend0

[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(F;m 1)
                                                                                         else n
                                                                                         fi x.x;mk_lambdas(G;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 then else fi  eq_int: (i =z 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_plus: + 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_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
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(F;m  -  1)  else  L  n  fi  ;\mlambda{}x.x;mk\_lambdas(G;m);0;m
                                              +  1))



Date html generated: 2016_05_15-PM-02_12_57
Last ObjectModification: 2016_01_15-PM-10_19_34

Theory : untyped!computation


Home Index