---

Step * of Lemma accum_split_iseg2

No Annotations
∀[T,A:Type].
  ∀x:A. ∀g:(T List × A) ⟶ A. ∀f:(T List × A) ⟶ 𝔹. ∀L1,L2:T List.
    (L1 ≤ L2
    ⇒ (∀LL1,LL2:(T List × A) List. ∀X,Y:T List. ∀z1,z2:A.
          (((LL1 = LL2 ∈ ((T List × A) List)) ∧ X ≤ Y ∧ (z1 = z2 ∈ A))
             ∨ (∃Z:T List
                 ∃ZZ:(T List × A) List. (((LL1 @ [<Z, z1> / ZZ]) = LL2 ∈ ((T List × A) List)) ∧ X ≤ Z))) supposing 
             ((accum_split(g;x;f;L2) = <LL2, Y, z2> ∈ ((T List × A) List × T List × A)) and 
             (accum_split(g;x;f;L1) = <LL1, X, z1> ∈ ((T List × A) List × T List × A)))))
BY
{ (InstLemma `accum_split_iseg` [] THEN RepeatFor 8 (ParallelLast') THEN Auto) }

1
1. [T] : Type
2. [A] : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. L1 : T List
7. L2 : T List
8. L1 ≤ L2
9. let LL1,X,z1 = accum_split(g;x;f;L1) in 
let LL2,Y,z2 = accum_split(g;x;f;L2) in 
((LL1 = LL2 ∈ ((T List × A) List)) ∧ X ≤ Y ∧ (z1 = z2 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((LL1 @ [<Z, z1> / ZZ]) = LL2 ∈ ((T List × A) List)) ∧ X ≤ Z))
10. LL1 : (T List × A) List
11. LL2 : (T List × A) List
12. X : T List
13. Y : T List
14. z1 : A
15. z2 : A
16. accum_split(g;x;f;L1) = <LL1, X, z1> ∈ ((T List × A) List × T List × A)
17. accum_split(g;x;f;L2) = <LL2, Y, z2> ∈ ((T List × A) List × T List × A)
⊢ ((LL1 = LL2 ∈ ((T List × A) List)) ∧ X ≤ Y ∧ (z1 = z2 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((LL1 @ [<Z, z1> / ZZ]) = LL2 ∈ ((T List × A) List)) ∧ X ≤ Z))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T,A:Type].
    \mforall{}x:A.  \mforall{}g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A.  \mforall{}f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L1,L2:T  List.
        (L1  \mleq{}  L2
        {}\mRightarrow{}  (\mforall{}LL1,LL2:(T  List  \mtimes{}  A)  List.  \mforall{}X,Y:T  List.  \mforall{}z1,z2:A.
                    (((LL1  =  LL2)  \mwedge{}  X  \mleq{}  Y  \mwedge{}  (z1  =  z2))
                          \mvee{}  (\mexists{}Z:T  List
                                  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((LL1  @  [<Z,  z1>  /  ZZ])  =  LL2)  \mwedge{}  X  \mleq{}  Z)))  supposing 
                          ((accum\_split(g;x;f;L2)  =  <LL2,  Y,  z2>)  and 
                          (accum\_split(g;x;f;L1)  =  <LL1,  X,  z1>))))


By

---

Latex:
(InstLemma  `accum\_split\_iseg`  []  THEN  RepeatFor  8  (ParallelLast')  THEN  Auto)

---

Home Index