Nuprl Lemma : sqle-list_ind-list_accum

[F:Base]
  ∀[G:Base]
    ∀[H,J:Base].
      ∀as,b1,b2:Base.
        G[b1;rec-case(as) of
             [] => b2
             h::t =>
              r.J[h;r]] ≤ F[accumulate (with value and list item a):
                             H[v;a]
                            over list:
                              as
                            with starting value:
                             b1)] 
        supposing ∀x:Base. (G[x;b2] ≤ F[x]) 
      supposing ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c]) 
    supposing ∀z:Base. strict1(λx.G[z;x]) 
  supposing strict1(λx.F[x])


Proof




Definitions occuring in Statement :  list_accum: list_accum list_ind: list_ind strict1: strict1(F) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] lambda: λx.A[x] base: Base sqle: s ≤ t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s] nat: implies:  Q false: False ge: i ≥  guard: {T} top: Top strict1: strict1(F) and: P ∧ Q cand: c∧ B not: ¬A squash: T or: P ∨ Q decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtract: m subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) true: True nat_plus: + so_apply: x[s1;s2] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] has-value: (a)↓ pi1: fst(t) pi2: snd(t) list_ind: list_ind list_accum: list_accum
Lemmas referenced :  le_wf le_weakening2 fixpoint-upper-bound bottom-sqle has-value-implies-dec-isaxiom-2 top_wf has-value-implies-dec-ispair-2 lifting-strict-isaxiom lifting-strict-ispair lifting-strict-callbyvalue fun_exp_unroll_1 int_subtype_base cbv_sqle strict1-strict4 nat_wf le-add-cancel add-zero add_functionality_wrt_le add-commutes add-swap add-associates minus-minus minus-add minus-one-mul-top zero-add minus-one-mul condition-implies-le less-iff-le not-ge-2 false_wf subtract_wf decidable__le is-exception_wf has-value_wf_base exception-not-bottom bottom_diverge strictness-apply fun_exp0_lemma less_than_wf ge_wf less_than_irreflexivity less_than_transitivity1 nat_properties strict1_wf sqle_wf_base base_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation axiomSqleEquality hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality baseApply closedConclusion baseClosed hypothesisEquality dependent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination voidEquality productElimination divergentSqle imageElimination unionElimination independent_pairFormation addEquality applyEquality intEquality minusEquality dependent_set_memberEquality callbyvalueIspair sqleTransitivity ispairExceptionCases exceptionSqequal sqleReflexivity fixpointLeast sqleRule

Latex:
\mforall{}[F:Base]
    \mforall{}[G:Base]
        \mforall{}[H,J:Base].
            \mforall{}as,b1,b2:Base.
                G[b1;rec-case(as)  of
                          []  =>  b2
                          h::t  =>
                            r.J[h;r]]  \mleq{}  F[accumulate  (with  value  v  and  list  item  a):
                                                          H[v;a]
                                                        over  list:
                                                            as
                                                        with  starting  value:
                                                          b1)] 
                supposing  \mforall{}x:Base.  (G[x;b2]  \mleq{}  F[x]) 
            supposing  \mforall{}a,b,c:Base.    (G[b;J[a;c]]  \mleq{}  G[H[b;a];c]) 
        supposing  \mforall{}z:Base.  strict1(\mlambda{}x.G[z;x]) 
    supposing  strict1(\mlambda{}x.F[x])



Date html generated: 2016_05_14-AM-06_28_10
Last ObjectModification: 2016_01_14-PM-08_27_29

Theory : list_0


Home Index