---

Step * 1 1 1 of Lemma list_split_iseg


1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. l : T List
4. v1 : T List List
5. v2 : T List
6. v3 : T List List
7. v4 : T List
⊢ (accumulate (with value p and list item v):
    let LL,L2 = p 
    in if null(L2) then <LL, [v]>
       if f L2 then <LL @ [L2], [v]>
       else <LL, L2 @ [v]>
       fi 
   over list:
     l
   with starting value:
    <v1, v2>)
= <v3, v4>
∈ (T List List × (T List)))
⇒ (((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
   ∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z)))
BY
{ xxx(RepeatFor 5 (MoveToConcl (-1)) THEN (BLemma `last_induction`  THENA Auto) THEN Reduce 0 THEN Auto)xxx }

1
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. v1 : T List List
4. v2 : T List
5. v3 : T List List
6. v4 : T List
7. <v1, v2> = <v3, v4> ∈ (T List List × (T List))
⊢ ((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z))

2
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. ys : T List
4. y : T
5. ∀v1:T List List. ∀v2:T List. ∀v3:T List List. ∀v4:T List.
     ((accumulate (with value p and list item v):
        let LL,L2 = p 
        in if null(L2) then <LL, [v]>
           if f L2 then <LL @ [L2], [v]>
           else <LL, L2 @ [v]>
           fi 
       over list:
         ys
       with starting value:
        <v1, v2>)
     = <v3, v4>
     ∈ (T List List × (T List)))
     ⇒ (((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
        ∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z))))
6. v1 : T List List
7. v2 : T List
8. v3 : T List List
9. v4 : T List
10. accumulate (with value p and list item v):
     let LL,L2 = p 
     in if null(L2) then <LL, [v]>
        if f L2 then <LL @ [L2], [v]>
        else <LL, L2 @ [v]>
        fi 
    over list:
      ys @ [y]
    with starting value:
     <v1, v2>)
= <v3, v4>
∈ (T List List × (T List))
⊢ ((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  l  :  T  List
4.  v1  :  T  List  List
5.  v2  :  T  List
6.  v3  :  T  List  List
7.  v4  :  T  List
\mvdash{}  (accumulate  (with  value  p  and  list  item  v):
        let  LL,L2  =  p 
        in  if  null(L2)  then  <LL,  [v]>
              if  f  L2  then  <LL  @  [L2],  [v]>
              else  <LL,  L2  @  [v]>
              fi 
      over  list:
          l
      with  starting  value:
        <v1,  v2>)
=  <v3,  v4>)
{}\mRightarrow{}  (((v1  =  v3)  \mwedge{}  v2  \mleq{}  v4)  \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((v1  @  [Z  /  ZZ])  =  v3)  \mwedge{}  v2  \mleq{}  Z)))


By

---

Latex:
xxx(RepeatFor  5  (MoveToConcl  (-1))
        THEN  (BLemma  `last\_induction`    THENA  Auto)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index