---

Step * 2 1 2 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(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))))
BY
{ xxxMoveToConcl (-1)xxx }

1
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) ⟶ 𝔹
⊢ ↑(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(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  \mneg{}\muparrow{}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))))


By

---

Latex:
xxxMoveToConcl  (-1)xxx

---

Home Index