Nuprl Lemma : callbyvalueall-seq-extend

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


Proof




Definitions occuring in Statement :  mk_applies: mk_applies(F;G;m) mk_lambdas: mk_lambdas(F;m) callbyvalueall-seq: callbyvalueall-seq(L;G;F;n;m) int_seg: {i..j-} 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 :  exists: x:A. B[x] member: t ∈ T nat: uall: [x:A]. B[x] nat_plus: + int_seg: {i..j-} guard: {T} lelt: i ≤ j < k and: P ∧ Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top prop: sq_type: SQType(T) squash: T true: True subtype_rel: A ⊆B iff: ⇐⇒ Q ge: i ≥  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 ∈  mk_applies: mk_applies(F;G;m) so_apply: x[s] mk_lambdas: mk_lambdas(F;m) le: A ≤ B rev_implies:  Q subtract: m less_than': less_than'(a;b)
Lemmas referenced :  subtract_wf int_seg_properties nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf itermAdd_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_less_lemma int_term_value_add_lemma int_formula_prop_wf le_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma equal_wf subtype_base_sq int_subtype_base less_than_wf squash_wf true_wf subtype_rel_self iff_weakening_equal nat_properties ge_wf int_seg_wf nat_plus_wf top_wf add-zero le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot eq_int_wf assert_of_eq_int neg_assert_of_eq_int decidable__lt lelt_wf primrec1_lemma primrec0_lemma mk_applies_lambdas1 add-subtract-cancel mk_applies_lambdas mk_applies_lambdas2 false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates le-add-cancel assert_wf bnot_wf not_wf equal-wf-base mk_applies_unroll bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot mk_applies_fun
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_pairFormation dependent_set_memberEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality natural_numberEquality addEquality productElimination dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation instantiate cumulativity equalityTransitivity equalitySymmetry applyEquality imageElimination imageMemberEquality baseClosed universeEquality intWeakElimination lambdaFormation sqequalAxiom isect_memberFormation equalityElimination promote_hyp minusEquality impliesFunctionality

Latex:
\mforall{}[F,G,L,K:Top].  \mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (callbyvalueall-seq(L;\mlambda{}f.mk\_applies(f;K;n);mk\_lambdas(\mlambda{}out.let  x  \mleftarrow{}{}  F[out]
                                                                                                                          in  G[x];m  -  1);n;m) 
    \msim{}  callbyvalueall-seq(\mlambda{}n.if  (n  =\msubz{}  m)  then  mk\_lambdas(F;m  -  1)  else  L  n  fi  ;\mlambda{}f.mk\_applies(f;K;n)
                                              ;mk\_lambdas(G;m);n;m  +  1))



Date html generated: 2018_05_21-PM-06_22_10
Last ObjectModification: 2018_05_19-PM-05_29_27

Theory : untyped!computation


Home Index