---

Step * of Lemma list_accum_proper_iseg_inv

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[R:A ⟶ A ⟶ ℙ]
      (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 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)])))
BY
{ xxx(Auto
      THEN D -1
      THEN D -2
      THEN (HypSubst' -2 0 THEN Auto)
      THEN RWO "list_accum_append" 0
      THEN Auto
      THEN GenConclAtAddr [2]
      THEN ThinVar `a'
      THEN RenameVar `a' (-1)
      THEN DVar `l'
      THEN All (RWO "append-nil")
      THEN Auto
      THEN Reduce 0
      THEN ThinVar `L1'
      THEN ThinVar `L2')xxx }

1
1. [T] : Type
2. [A] : Type
3. f : A ⟶ T ⟶ A
4. [R] : A ⟶ A ⟶ ℙ
5. Trans(A;a,b.R[a;b])
6. ∀a:A. ∀x:T.  R[a;f[a;x]]
7. u : T
8. v : T List
9. a : A
⊢ R[a;accumulate (with value a and list item x):
       f[a;x]
      over list:
        v
      with starting value:
       f[a;u])]

---

Latex:

---

Latex:
\mforall{}[T,A:Type].
    \mforall{}f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
        \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
            (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  <  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)])))


By

---

Latex:
xxx(Auto
        THEN  D  -1
        THEN  D  -2
        THEN  (HypSubst'  -2  0  THEN  Auto)
        THEN  RWO  "list\_accum\_append"  0
        THEN  Auto
        THEN  GenConclAtAddr  [2]
        THEN  ThinVar  `a'
        THEN  RenameVar  `a'  (-1)
        THEN  DVar  `l'
        THEN  All  (RWO  "append-nil")
        THEN  Auto
        THEN  Reduce  0
        THEN  ThinVar  `L1'
        THEN  ThinVar  `L2')xxx

---

Home Index