Nuprl Lemma : list_accum_iseg_inv

[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[R:A ⟶ A ⟶ ℙ]
      (Refl(A;a,b.R[a;b])
       Trans(A;a,b.R[a;b])
       (∀a:A. ∀x:T.  R[a;f[a;x]])
       (∀a:A. ∀L1,L2:T List.
            (L1 ≤ L2
             R[accumulate (with value and list item x):
                  f[a;x]
                 over list:
                   L1
                 with starting value:
                  a);accumulate (with value and list item x):
                      f[a;x]
                     over list:
                       L2
                     with starting value:
                      a)])))


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 list_accum: list_accum list: List trans: Trans(T;x,y.E[x; y]) refl: Refl(T;x,y.E[x; y]) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q iseg: l1 ≤ l2 exists: x:A. B[x] member: t ∈ T prop: subtype_rel: A ⊆B uimplies: supposing a top: Top so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s] trans: Trans(T;x,y.E[x; y]) guard: {T} refl: Refl(T;x,y.E[x; y])
Lemmas referenced :  length_wf_nat equal_wf nat_wf list_accum_append subtype_rel_list top_wf list_accum_wf iseg_wf list_wf all_wf trans_wf refl_wf list_induction list_accum_nil_lemma list_accum_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut dependent_set_memberEquality hypothesis introduction extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule applyEquality independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache functionExtensionality rename equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality setElimination functionEquality universeEquality

Latex:
\mforall{}[T,A:Type].
    \mforall{}f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
        \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
            (Refl(A;a,b.R[a;b])
            {}\mRightarrow{}  Trans(A;a,b.R[a;b])
            {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}x:T.    R[a;f[a;x]])
            {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}L1,L2:T  List.
                        (L1  \mleq{}  L2
                        {}\mRightarrow{}  R[accumulate  (with  value  a  and  list  item  x):
                                    f[a;x]
                                  over  list:
                                      L1
                                  with  starting  value:
                                    a);accumulate  (with  value  a  and  list  item  x):
                                            f[a;x]
                                          over  list:
                                              L2
                                          with  starting  value:
                                            a)])))



Date html generated: 2018_05_21-PM-06_42_16
Last ObjectModification: 2017_07_26-PM-04_54_20

Theory : general


Home Index