Nuprl Lemma : simple-cbva-seq-list-case1

[F,L1,L2,a:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ].
  (simple-cbva-seq(λn.if (n) < (m1)
                         then L1 n
                         else mk_lambdas(λout.if m1=m2
                                              then mk_lambdas(λo1.(out o1);m2 1)
                                              else (L2 (n m1));m1 1);F;(m1 m2) 1) 
  simple-cbva-seq(λn.if (n) < (m1)
                          then L1 n
                          else if (n) < (m1 m2)
                                  then mk_lambdas(L2 (n m1);m1)
                                  else mk_lambdas(λout1.mk_lambdas(λout2.(out1 out2);m2 1);m1 1);F;(m1 m2) 1))


Proof




Definitions occuring in Statement :  simple-cbva-seq: simple-cbva-seq(L;F;m) mk_lambdas: mk_lambdas(F;m) nat_plus: + nat: uall: [x:A]. B[x] top: Top less: if (a) < (b)  then c  else d int_eq: if a=b then else d 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: + nat: 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  ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: bfalse: ff subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b le: A ≤ B less_than': less_than'(a;b) decidable: Dec(P) mk_applies: mk_applies(F;G;m) int_seg: {i..j-} lelt: i ≤ j < k rev_implies:  Q iff: ⇐⇒ Q lt_int: i <j so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] has-value: (a)↓ less_than: a < b true: True squash: T so_apply: x[s1;s2]
Lemmas referenced :  eq_int_wf eqtt_to_assert assert_of_eq_int nat_properties nat_plus_properties full-omega-unsat intformand_wf intformeq_wf itermAdd_wf itermVar_wf itermConstant_wf intformle_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_less_lemma int_formula_prop_wf eqff_to_assert set_subtype_base le_wf int_subtype_base less_than_wf bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int nat_wf nat_plus_wf istype-top add-subtract-cancel istype-false decidable__le intformnot_wf int_formula_prop_not_lemma primrec0_lemma decidable__lt decidable__equal_int itermSubtract_wf int_term_value_subtract_lemma lt_int_wf assert_of_lt_int iff_weakening_uiff assert_wf callbyvalueall_seq-seq callbyvalueall_seq-decomp-last less_as_ite callbyvalueall_seq-fun2 lifting-strict-less strict4-decide has-value_wf_base is-exception_wf callbyvalueall_seq-fun4 mk_lambdas_unroll2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin addEquality setElimination rename hypothesisEquality hypothesis natural_numberEquality inhabitedIsType lambdaFormation_alt unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination independent_pairFormation universeIsType equalityIsType2 baseApply closedConclusion baseClosed applyEquality intEquality promote_hyp instantiate cumulativity because_Cache equalityIsType1 isect_memberFormation_alt axiomSqEquality dependent_set_memberEquality_alt productIsType int_eqReduceTrueSq sqequalSqle divergentSqle callbyvalueLess lessCases imageMemberEquality imageElimination sqleReflexivity lessExceptionCases axiomSqleEquality exceptionSqequal exceptionLess

Latex:
\mforall{}[F,L1,L2,a:Top].  \mforall{}[m1:\mBbbN{}\msupplus{}].  \mforall{}[m2:\mBbbN{}].
    (simple-cbva-seq(\mlambda{}n.if  (n)  <  (m1)
                                                  then  L1  a  n
                                                  else  mk\_lambdas(\mlambda{}out.if  n  -  m1=m2
                                                                                            then  mk\_lambdas(\mlambda{}o1.(out  +  o1);m2  -  1)
                                                                                            else  (L2  a  (n  -  m1));m1  -  1);F;(m1  +  m2)  +  1) 
    \msim{}  simple-cbva-seq(\mlambda{}n.if  (n)  <  (m1)
                                                    then  L1  a  n
                                                    else  if  (n)  <  (m1  +  m2)
                                                                    then  mk\_lambdas(L2  a  (n  -  m1);m1)
                                                                    else  mk\_lambdas(\mlambda{}out1.mk\_lambdas(\mlambda{}out2.(out1  +  out2);m2  -  1);m1 
                                                                              -  1);F;(m1  +  m2)  +  1))



Date html generated: 2019_10_15-AM-10_59_09
Last ObjectModification: 2018_10_11-PM-09_50_52

Theory : untyped!computation


Home Index