---

Step * 2 1 1 of Lemma list_split_prefix

.....equality..... 
1. T : Type
2. ys : T List
3. y : T
4. ∀[g:(T List) ⟶ 𝔹]. ↑(g (snd(list_split(g;concat(fst(list_split(g;ys))))))) supposing ¬↑null(fst(list_split(g;ys)))
5. g : (T List) ⟶ 𝔹
6. ↑(g (snd(list_split(g;concat(fst(list_split(g;ys))))))) supposing ¬↑null(fst(list_split(g;ys)))
⊢ list_split(g;ys @ [y]) ~ accumulate (with value p and list item v):
                            let LL,L2 = p 
                            in if null(L2) then <LL, [v]>
                               if g L2 then <LL @ [L2], [v]>
                               else <LL, L2 @ [v]>
                               fi 
                           over list:
                             [y]
                           with starting value:
                            list_split(g;ys))
BY
{ xxx(Unfold `list_split` 0 THEN (RWO "list_accum_append" 0 THENA Auto) THEN Fold `list_split` 0 THEN EqCD)xxx }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  ys  :  T  List
3.  y  :  T
4.  \mforall{}[g:(T  List)  {}\mrightarrow{}  \mBbbB{}]
          \muparrow{}(g  (snd(list\_split(g;concat(fst(list\_split(g;ys)))))))  supposing  \mneg{}\muparrow{}null(fst(list\_split(g;ys)))
5.  g  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
6.  \muparrow{}(g  (snd(list\_split(g;concat(fst(list\_split(g;ys)))))))  supposing  \mneg{}\muparrow{}null(fst(list\_split(g;ys)))
\mvdash{}  list\_split(g;ys  @  [y])  \msim{}  accumulate  (with  value  p  and  list  item  v):
                                                        let  LL,L2  =  p 
                                                        in  if  null(L2)  then  <LL,  [v]>
                                                              if  g  L2  then  <LL  @  [L2],  [v]>
                                                              else  <LL,  L2  @  [v]>
                                                              fi 
                                                      over  list:
                                                          [y]
                                                      with  starting  value:
                                                        list\_split(g;ys))


By

---

Latex:
xxx(Unfold  `list\_split`  0
        THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
        THEN  Fold  `list\_split`  0
        THEN  EqCD)xxx

---

Home Index