### Nuprl Lemma : cbva_seq-sqequal-n

`∀L:Top. ∀F1,F2:Base. ∀m,n:ℕ.  ((F1 ~n + 1 F2) `` (cbva_seq(L; F1; m) ~n cbva_seq(L; F2; m)))`

Proof

Definitions occuring in Statement :  cbva_seq: `cbva_seq(L; F; m)` nat: `ℕ` top: `Top` all: `∀x:A. B[x]` implies: `P `` Q` add: `n + m` natural_number: `\$n` base: `Base` sqequal_n: `s ~n t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` cbva_seq: `cbva_seq(L; F; m)` exists: `∃x:A. B[x]` true: `True` prop: `ℙ` mk_applies: `mk_applies(F;G;m)` top: `Top` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` uall: `∀[x:A]. B[x]` guard: `{T}` ge: `i ≥ j ` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` sq_type: `SQType(T)` callbyvalueall_seq: `callbyvalueall_seq(L;G;F;n;m)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` callbyvalueall: callbyvalueall subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  decidable__lt true_wf primrec0_lemma false_wf le_wf nat_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf intformeq_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_constant_lemma int_formula_prop_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma decidable__equal_int itermAdd_wf int_term_value_add_lemma equal_wf subtype_base_sq int_subtype_base le_int_wf bool_wf eqtt_to_assert assert_of_le_int add-subtract-cancel intformless_wf int_formula_prop_less_lemma eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot base_wf set_subtype_base all_wf sqequal_n_wf set_wf less_than_wf primrec-wf2 top_wf mk_applies_roll
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequal_n rule thin introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination natural_numberEquality addEquality setElimination rename hypothesisEquality hypothesis unionElimination promote_hyp dependent_pairFormation baseClosed productElimination sqequalRule isect_memberEquality voidElimination voidEquality dependent_set_memberEquality independent_pairFormation isectElimination equalityTransitivity equalitySymmetry applyLambdaEquality independent_isectElimination lambdaEquality int_eqEquality intEquality computeAll because_Cache instantiate cumulativity independent_functionElimination equalityElimination sqequalnReflexivity baseApply closedConclusion applyEquality sqequalZero

Latex:
\mforall{}L:Top.  \mforall{}F1,F2:Base.  \mforall{}m,n:\mBbbN{}.    ((F1  \msim{}n  +  1  F2)  {}\mRightarrow{}  (cbva\_seq(L;  F1;  m)  \msim{}n  cbva\_seq(L;  F2;  m)))

Date html generated: 2017_10_01-AM-08_42_52
Last ObjectModification: 2017_07_26-PM-04_29_23

Theory : untyped!computation

Home Index