---

Step * 2 2 1 1 of Lemma list_split_wf


1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v : {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;firstn(||L|| - 1;L);LL;L2;f)} 
⊢ accumulate (with value p and list item v):
   let LL,L2 = p 
   in if null(L2) then <LL, [v]>
      if f L2 then <LL @ [L2], [v]>
      else <LL, L2 @ [v]>
      fi 
  over list:
    [last(L)]
  with starting value:
   v) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;firstn(||L|| - 1;L) @ [last(L)];LL;L2;f)} 
BY
{ (D -1
   THEN RepeatFor 2 ((D -2 THEN All Reduce))
   THEN RepUR ``is_list_splitting`` -1
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN Try ((SplitOnConclITE THENA Auto))
   THEN RepUR ``is_list_splitting`` 0
   THEN Auto
   THEN All (RWO "append-nil")
   THEN Auto
   THEN Try (((RWO "iseg_single" (-2) THENM D -2) THEN Auto))) }

1
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ↑(f [u / v])
⊢ (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1 @ [[u / v]]) @ [last(L)]) ∈ (T List)

2
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ↑(f [u / v])
14. (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1 @ [[u / v]]) @ [last(L)]) ∈ (T List)
⊢ (∀L'∈v1 @ [[u / v]].(↑(f L'))
      ∧ (¬↑null(L'))
      ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))

3
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ¬↑(f [u / v])
⊢ (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1) @ [u / (v @ [last(L)])]) ∈ (T List)

4
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ¬↑(f [u / v])
14. (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1) @ [u / (v @ [last(L)])]) ∈ (T List)
15. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
16. (¬↑null(firstn(||L|| - 1;L) @ [last(L)])) ⇒ (¬False)
17. S : T List
18. ¬↑null(S)
19. S ≤ [u / (v @ [last(L)])]
20. ¬(S = [u / (v @ [last(L)])] ∈ (T List))
⊢ ¬↑(f S)

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  n  :  \mBbbN{}
4.  L  :  T  List
5.  \mneg{}\muparrow{}null(L)
6.  v  :  \{p:T  List  List  \mtimes{}  (T  List)| 
                let  LL,L2  =  p 
                in  is\_list\_splitting(T;firstn(||L||  -  1;L);LL;L2;f)\} 
\mvdash{}  accumulate  (with  value  p  and  list  item  v):
      let  LL,L2  =  p 
      in  if  null(L2)  then  <LL,  [v]>
            if  f  L2  then  <LL  @  [L2],  [v]>
            else  <LL,  L2  @  [v]>
            fi 
    over  list:
        [last(L)]
    with  starting  value:
      v)  \mmember{}  \{p:T  List  List  \mtimes{}  (T  List)| 
                  let  LL,L2  =  p 
                  in  is\_list\_splitting(T;firstn(||L||  -  1;L)  @  [last(L)];LL;L2;f)\} 


By

---

Latex:
(D  -1
  THEN  RepeatFor  2  ((D  -2  THEN  All  Reduce))
  THEN  RepUR  ``is\_list\_splitting``  -1
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((SplitOnConclITE  THENA  Auto))
  THEN  RepUR  ``is\_list\_splitting``  0
  THEN  Auto
  THEN  All  (RWO  "append-nil")
  THEN  Auto
  THEN  Try  (((RWO  "iseg\_single"  (-2)  THENM  D  -2)  THEN  Auto)))

---

Home Index