---

Step * 2 1 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) ⟶ 𝔹
⊢ ↑(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
{ xxx(GenConclAtAddr [1;1;1;1;1;1] THEN D -2 THEN D -3 THEN Reduce 0)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) ⟶ 𝔹
6. v1 : T List List
7. v2 : T List
8. [%5] : let LL,L2 = <v1, v2> 
          in is_list_splitting(T;ys;LL;L2;g)
9. list_split(g;ys) = <v1, v2> ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;ys;LL;L2;g)} 
⊢ ↑(g (snd(list_split(g;concat(v1))))) supposing ¬↑null(v1)
⇒ ↑(g 
     (snd(list_split(g;concat(fst(if null(v2) then <v1, [y]>
     if g v2 then <v1 @ [v2], [y]>
     else <v1, v2 @ [y]>
     fi )))))) 
   supposing ¬↑null(fst(if null(v2) then <v1, [y]>
   if g v2 then <v1 @ [v2], [y]>
   else <v1, v2 @ [y]>
   fi ))

---

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{}
\mvdash{}  \muparrow{}(g  (snd(list\_split(g;concat(fst(list\_split(g;ys)))))))  supposing  \mneg{}\muparrow{}null(fst(list\_split(g;ys)))
{}\mRightarrow{}  \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:
xxx(GenConclAtAddr  [1;1;1;1;1;1]  THEN  D  -2  THEN  D  -3  THEN  Reduce  0)xxx

---

Home Index