---

Step * of Lemma accum_split_prefix

∀[A,T:Type]. ∀[x:A]. ∀[g:(T List × A) ⟶ A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[L:T List].
  ↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;L)))))))) 
  supposing ¬↑null(fst(accum_split(g;x;f;L)))
BY
{ xxx(Auto THEN RepeatFor 2 (MoveToConcl (-1)) THEN (BLemma `last_induction` THENA Auto))xxx }

1
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
⊢ (¬↑null(fst(accum_split(g;x;f;[]))))
⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;[])))))))))

2
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]))))))))))

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[x:A].  \mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    \muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));fst(accum\_split(g;x;f;L)))))))) 
    supposing  \mneg{}\muparrow{}null(fst(accum\_split(g;x;f;L)))


By

---

Latex:
xxx(Auto  THEN  RepeatFor  2  (MoveToConcl  (-1))  THEN  (BLemma  `last\_induction`  THENA  Auto))xxx

---

Home Index