---

Step * 2 1 of Lemma accum_split_prefix


1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. (¬↑null(fst(accum_split(g;x;f;ys))))
⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;ys)))))))))
⊢ (¬↑null(fst(accum_split(g;x;f;ys @ [y]))))
⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;ys @ [y])))))))))
BY
{ xxx(Unfold `accum_split` 0
      THEN (RWO "list_accum_append" 0 THENA Auto)
      THEN Fold `accum_split` 0
      THEN MoveToConcl (-1)
      THEN GenConclAtAddr [1;1;1;1;1;1]
      THEN D -2
      THEN RepeatFor 2 (D -3)
      THEN Reduce 0
      THEN OldAutoBoolCase ⌜null(v3)⌝⋅
      THEN OldAutoBoolCase ⌜f <v3, v4>⌝⋅
      THEN Auto)xxx }

1
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. v1 : (T List × A) List
9. v3 : T List
10. v4 : A
11. let LL,L2 = <v1, v3, v4> 
    in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
12. accum_split(g;x;f;ys)
= <v1, v3, v4>
∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;ys;LL;L2;f;g;x)} 
13. ¬(v3 = [] ∈ (T List))
14. ↑(f <v3, v4>)
15. (¬↑null(v1)) ⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));v1)))))))
16. ¬↑null(v1 @ [<v3, v4>])
⊢ ↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));v1 @ [<v3, v4>]))))))

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  x  :  A
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
6.  ys  :  T  List
7.  y  :  T
8.  (\mneg{}\muparrow{}null(fst(accum\_split(g;x;f;ys))))
{}\mRightarrow{}  (\muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));fst(accum\_split(g;x;f;ys)))))))))
\mvdash{}  (\mneg{}\muparrow{}null(fst(accum\_split(g;x;f;ys  @  [y]))))
{}\mRightarrow{}  (\muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));fst(accum\_split(g;x;f;ys  @  [y])))))))))


By

---

Latex:
xxx(Unfold  `accum\_split`  0
        THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
        THEN  Fold  `accum\_split`  0
        THEN  MoveToConcl  (-1)
        THEN  GenConclAtAddr  [1;1;1;1;1;1]
        THEN  D  -2
        THEN  RepeatFor  2  (D  -3)
        THEN  Reduce  0
        THEN  OldAutoBoolCase  \mkleeneopen{}null(v3)\mkleeneclose{}\mcdot{}
        THEN  OldAutoBoolCase  \mkleeneopen{}f  <v3,  v4>\mkleeneclose{}\mcdot{}
        THEN  Auto)xxx

---

Home Index