---

Step * 1 1 of Lemma accum_split_iseg


1. [T] : Type
2. [A] : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. L1 : T List
7. L2 : T List
8. l : T List
9. L2 = (L1 @ l) ∈ (T List)
10. v1 : (T List × A) List
11. v3 : T List
12. v4 : A
13. accum_split(g;x;f;L1) = <v1, v3, v4> ∈ ((T List × A) List × T List × A)
14. v5 : (T List × A) List
15. v7 : T List
16. v8 : A
17. accum_split(g;x;f;L2) = <v5, v7, v8> ∈ ((T List × A) List × T List × A)
18. 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:
      l
    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
{ (MoveToConcl (-1)
   THEN All Thin
   THEN RepeatFor 7 (MoveToConcl (-1))
   THEN (BLemma `last_induction`  THENA Auto)
   THEN Reduce 0
   THEN Auto) }

1
1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. v1 : (T List × A) List
6. v3 : T List
7. v4 : A
8. v5 : (T List × A) List
9. v7 : T List
10. v8 : A
11. <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))

2
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))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  x  :  A
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
6.  L1  :  T  List
7.  L2  :  T  List
8.  l  :  T  List
9.  L2  =  (L1  @  l)
10.  v1  :  (T  List  \mtimes{}  A)  List
11.  v3  :  T  List
12.  v4  :  A
13.  accum\_split(g;x;f;L1)  =  <v1,  v3,  v4>
14.  v5  :  (T  List  \mtimes{}  A)  List
15.  v7  :  T  List
16.  v8  :  A
17.  accum\_split(g;x;f;L2)  =  <v5,  v7,  v8>
18.  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:
            l
        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:
(MoveToConcl  (-1)
  THEN  All  Thin
  THEN  RepeatFor  7  (MoveToConcl  (-1))
  THEN  (BLemma  `last\_induction`    THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index