---

Step * 1 1 2 of Lemma accum_split_iseg


1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. ys : T List
6. y : T
7. ∀v1:(T List × A) List. ∀v3:T List. ∀v4:A. ∀v5:(T List × A) List. ∀v7:T List. ∀v8:A.
     ((accumulate (with value p and list item v):
        let LL,L2,z = p in 
        if null(L2) then <LL, [v], z>
        if f <L2, z> then <LL @ [<L2, z>], [v], g <L2, z>>
        else <LL, L2 @ [v], z>
        fi 
       over list:
         ys
       with starting value:
        <v1, v3, v4>)
     = <v5, v7, v8>
     ∈ ((T List × A) List × T List × A))
     ⇒ (((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
        ∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z))))
8. v1 : (T List × A) List
9. v3 : T List
10. v4 : A
11. v5 : (T List × A) List
12. v7 : T List
13. v8 : A
14. accumulate (with value p and list item v):
     let LL,L2,z = p in 
     if null(L2) then <LL, [v], z>
     if f <L2, z> then <LL @ [<L2, z>], [v], g <L2, z>>
     else <LL, L2 @ [v], z>
     fi 
    over list:
      ys @ [y]
    with starting value:
     <v1, v3, v4>)
= <v5, v7, v8>
∈ ((T List × A) List × T List × A)
⊢ ((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
BY
{ ((RWO "list_accum_append" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;2;2] THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN (FHyp 7 [-1] THENA Auto)
   THEN Thin 7
   THEN Thin (-2)
   THEN Reduce 0) }

1
1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. ys : T List
6. y : T
7. v1 : (T List × A) List
8. v3 : T List
9. v4 : A
10. v5 : (T List × A) List
11. v7 : T List
12. v8 : A
13. v9 : (T List × A) List
14. v11 : T List
15. v12 : A
16. ((v1 = v9 ∈ ((T List × A) List)) ∧ v3 ≤ v11 ∧ (v4 = v12 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v9 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
⊢ (if null(v11) then <v9, [y], v12>
if f <v11, v12> then <v9 @ [<v11, v12>], [y], g <v11, v12>>
else <v9, v11 @ [y], v12>
fi 
= <v5, v7, v8>
∈ ((T List × A) List × T List × A))
⇒ (((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
   ∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
4.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
5.  ys  :  T  List
6.  y  :  T
7.  \mforall{}v1:(T  List  \mtimes{}  A)  List.  \mforall{}v3:T  List.  \mforall{}v4:A.  \mforall{}v5:(T  List  \mtimes{}  A)  List.  \mforall{}v7:T  List.  \mforall{}v8:A.
          ((accumulate  (with  value  p  and  list  item  v):
                let  LL,L2,z  =  p  in 
                if  null(L2)  then  <LL,  [v],  z>
                if  f  <L2,  z>  then  <LL  @  [<L2,  z>],  [v],  g  <L2,  z>>
                else  <LL,  L2  @  [v],  z>
                fi 
              over  list:
                  ys
              with  starting  value:
                <v1,  v3,  v4>)
          =  <v5,  v7,  v8>)
          {}\mRightarrow{}  (((v1  =  v5)  \mwedge{}  v3  \mleq{}  v7  \mwedge{}  (v4  =  v8))
                \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((v1  @  [<Z,  v4>  /  ZZ])  =  v5)  \mwedge{}  v3  \mleq{}  Z))))
8.  v1  :  (T  List  \mtimes{}  A)  List
9.  v3  :  T  List
10.  v4  :  A
11.  v5  :  (T  List  \mtimes{}  A)  List
12.  v7  :  T  List
13.  v8  :  A
14.  accumulate  (with  value  p  and  list  item  v):
          let  LL,L2,z  =  p  in 
          if  null(L2)  then  <LL,  [v],  z>
          if  f  <L2,  z>  then  <LL  @  [<L2,  z>],  [v],  g  <L2,  z>>
          else  <LL,  L2  @  [v],  z>
          fi 
        over  list:
            ys  @  [y]
        with  starting  value:
          <v1,  v3,  v4>)
=  <v5,  v7,  v8>
\mvdash{}  ((v1  =  v5)  \mwedge{}  v3  \mleq{}  v7  \mwedge{}  (v4  =  v8))
\mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((v1  @  [<Z,  v4>  /  ZZ])  =  v5)  \mwedge{}  v3  \mleq{}  Z))


By

---

Latex:
((RWO  "list\_accum\_append"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;2;2]  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  (FHyp  7  [-1]  THENA  Auto)
  THEN  Thin  7
  THEN  Thin  (-2)
  THEN  Reduce  0)

---

Home Index