---

Step * 1 1 1 2 of Lemma list_split_iseg


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))
BY
{ xxx((RWO "list_accum_append" (-1) THENA Auto)
      THEN MoveToConcl (-1)
      THEN GenConclAtAddr [1;2;2]
      THEN D -2
      THEN (FHyp 5 [-1] THENA Auto)
      THEN Thin 5
      THEN Thin (-2)
      THEN Reduce 0)xxx }

1
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. ys : T List
4. y : T
5. v1 : T List List
6. v2 : T List
7. v3 : T List List
8. v4 : T List
9. v5 : T List List
10. v6 : T List
11. ((v1 = v5 ∈ (T List List)) ∧ v2 ≤ v6)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v5 ∈ (T List List)) ∧ v2 ≤ Z))
⊢ (if null(v6) then <v5, [y]>
if f v6 then <v5 @ [v6], [y]>
else <v5, v6 @ [y]>
fi 
= <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.  ys  :  T  List
4.  y  :  T
5.  \mforall{}v1:T  List  List.  \mforall{}v2:T  List.  \mforall{}v3:T  List  List.  \mforall{}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>)
          {}\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))))
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>
\mvdash{}  ((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((RWO  "list\_accum\_append"  (-1)  THENA  Auto)
        THEN  MoveToConcl  (-1)
        THEN  GenConclAtAddr  [1;2;2]
        THEN  D  -2
        THEN  (FHyp  5  [-1]  THENA  Auto)
        THEN  Thin  5
        THEN  Thin  (-2)
        THEN  Reduce  0)xxx

---

Home Index