---

Step * of Lemma list_split_one_one

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

1
1. T : Type
2. f : (T List) ⟶ 𝔹
3. X : T List
4. Y : T List
5. list_split(f;X) = list_split(f;Y) ∈ (T List List × (T List))
6. X = (concat(fst(list_split(f;X))) @ (snd(list_split(f;X)))) ∈ (T List)
7. Y = (concat(fst(list_split(f;Y))) @ (snd(list_split(f;Y)))) ∈ (T List)
⊢ X = Y ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:(T  List)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[X,Y:T  List].    X  =  Y  supposing  list\_split(f;X)  =  list\_split(f;Y)


By

---

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

---

Home Index