Nuprl Lemma : simple-cbva-seq-extend

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


Proof




Definitions occuring in Statement :  simple-cbva-seq: simple-cbva-seq(L;F;m) mk_lambdas: mk_lambdas(F;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 :  simple-cbva-seq: simple-cbva-seq(L;F;m) cbva-seq: cbva-seq(L;F;m) member: t ∈ T uall: [x:A]. B[x] nat_plus: + all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False nequal: a ≠ b ∈  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int nat_plus_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf itermAdd_wf int_term_value_add_lemma add-subtract-cancel callbyvalueall-seq-extend0 nat_plus_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule addEquality because_Cache dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination approximateComputation lambdaEquality int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation isect_memberFormation sqequalAxiom

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



Date html generated: 2018_05_21-PM-06_22_34
Last ObjectModification: 2018_05_19-PM-05_30_12

Theory : untyped!computation


Home Index