---

Step * 2 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) ⟶ 𝔹
⊢ ∀ys:T List. ∀y:T.
    (((¬↑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
{ xxxRepeatFor 3 ((D 0 THENA 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. (¬↑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])))))))))

---

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{}
\mvdash{}  \mforall{}ys:T  List.  \mforall{}y:T.
        (((\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))))))))))
        {}\mRightarrow{}  (\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:
xxxRepeatFor  3  ((D  0  THENA  Auto))xxx

---

Home Index