---

Step * 2 1 2 1 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. 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 ))
BY
{ xxxOldAutoBoolCase ⌜null(v2)⌝⋅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)} 
10. ¬(v2 = [] ∈ (T List))
⊢ ↑(g (snd(list_split(g;concat(v1))))) supposing ¬↑null(v1)
⇒ ↑(g (snd(list_split(g;concat(fst(if g v2 then <v1 @ [v2], [y]> else <v1, v2 @ [y]> fi )))))) 
   supposing ¬↑null(fst(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{}
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>
\mvdash{}  \muparrow{}(g  (snd(list\_split(g;concat(v1)))))  supposing  \mneg{}\muparrow{}null(v1)
{}\mRightarrow{}  \muparrow{}(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  \mneg{}\muparrow{}null(fst(if  null(v2)  then  <v1,  [y]>
      if  g  v2  then  <v1  @  [v2],  [y]>
      else  <v1,  v2  @  [y]>
      fi  ))


By

---

Latex:
xxxOldAutoBoolCase  \mkleeneopen{}null(v2)\mkleeneclose{}\mcdot{}xxx

---

Home Index