---

Step * of Lemma accum_split_one_one

∀[A,T:Type]. ∀[x:A]. ∀[g:(T List × A) ⟶ A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[X,Y:T List].
  X = Y ∈ (T List) supposing accum_split(g;x;f;X) = accum_split(g;x;f;Y) ∈ ((T List × A) List × T List × A)
BY
{ (Auto
   THEN (InstLemma `accum_split_inverse` [⌜A⌝;⌜T⌝;⌜x⌝;⌜g⌝;⌜f⌝;⌜X⌝;⌜fst(accum_split(g;x;f;X))⌝;
         ⌜fst(snd(accum_split(g;x;f;X)))⌝;⌜snd(snd(accum_split(g;x;f;X)))⌝]⋅
         THENA (Auto THEN GenConclAtAddr [2] THEN Auto THEN D -2 THEN RepeatFor 2 (D -3) THEN Reduce 0 THEN Auto)
         )
   THEN (InstLemma `accum_split_inverse` [⌜A⌝;⌜T⌝;⌜x⌝;⌜g⌝;⌜f⌝;⌜Y⌝;⌜fst(accum_split(g;x;f;Y))⌝;
         ⌜fst(snd(accum_split(g;x;f;Y)))⌝;⌜snd(snd(accum_split(g;x;f;Y)))⌝]⋅
         THENA (Auto THEN GenConclAtAddr [2] THEN Auto THEN D -2 THEN RepeatFor 2 (D -3) THEN Reduce 0 THEN Auto)
         )) }

1
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. X : T List
7. Y : T List
8. accum_split(g;x;f;X) = accum_split(g;x;f;Y) ∈ ((T List × A) List × T List × A)
9. X = (concat(map(λp.(fst(p));fst(accum_split(g;x;f;X)))) @ (fst(snd(accum_split(g;x;f;X))))) ∈ (T List)
10. Y = (concat(map(λp.(fst(p));fst(accum_split(g;x;f;Y)))) @ (fst(snd(accum_split(g;x;f;Y))))) ∈ (T List)
⊢ X = Y ∈ (T List)

---

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{}[X,Y:T  List].
    X  =  Y  supposing  accum\_split(g;x;f;X)  =  accum\_split(g;x;f;Y)


By

---

Latex:
(Auto
  THEN  (InstLemma  `accum\_split\_inverse`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}fst(accum\_split(g;x;f;X))\mkleeneclose{};
              \mkleeneopen{}fst(snd(accum\_split(g;x;f;X)))\mkleeneclose{};\mkleeneopen{}snd(snd(accum\_split(g;x;f;X)))\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  GenConclAtAddr  [2]
                            THEN  Auto
                            THEN  D  -2
                            THEN  RepeatFor  2  (D  -3)
                            THEN  Reduce  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `accum\_split\_inverse`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}fst(accum\_split(g;x;f;Y))\mkleeneclose{};
              \mkleeneopen{}fst(snd(accum\_split(g;x;f;Y)))\mkleeneclose{};\mkleeneopen{}snd(snd(accum\_split(g;x;f;Y)))\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  GenConclAtAddr  [2]
                            THEN  Auto
                            THEN  D  -2
                            THEN  RepeatFor  2  (D  -3)
                            THEN  Reduce  0
                            THEN  Auto)
              ))

---

Home Index