---

Step * 2 1 of Lemma list_split_prefix


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)))
⊢ ↑(g (snd(list_split(g;concat(fst(list_split(g;ys @ [y]))))))) supposing ¬↑null(fst(list_split(g;ys @ [y])))
BY
{ xxxSubst' 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)) 0xxx }

1
.....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))

2
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)))
⊢ ↑(g 
    (snd(list_split(g;concat(fst(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)))))))) 
  supposing ¬↑null(fst(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))))

---

Latex:

---

Latex:

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{}  \muparrow{}(g  (snd(list\_split(g;concat(fst(list\_split(g;ys  @  [y]))))))) 
    supposing  \mneg{}\muparrow{}null(fst(list\_split(g;ys  @  [y])))


By

---

Latex:
xxxSubst'  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))  0xxx

---

Home Index