---

Step * of Lemma accum_split_iseg

No Annotations
∀[T,A:Type].
  ∀x:A. ∀g:(T List × A) ⟶ A. ∀f:(T List × A) ⟶ 𝔹. ∀L1,L2:T List.
    (L1 ≤ L2
    ⇒ 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)))
BY
{ (Auto
   THEN RepeatFor 2 ((GenConclAtAddr [1] THEN D -2 THEN RepeatFor 2 (D -3) THEN All Reduce THEN Thin (-2)))
   THEN ∀h:hyp. ((EqTypeHD h THENM Thin (h+1)) THENA 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. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. accum_split(g;x;f;L1) = <v1, v3, v4> ∈ ((T List × A) List × T List × A)
13. v5 : (T List × A) List
14. v7 : T List
15. v8 : A
16. accum_split(g;x;f;L2) = <v5, v7, v8> ∈ ((T List × A) List × T List × A)
⊢ ((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ 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{}  let  LL1,X,z1  =  accum\_split(g;x;f;L1)  in 
              let  LL2,Y,z2  =  accum\_split(g;x;f;L2)  in 
              ((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)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((GenConclAtAddr  [1]
                                        THEN  D  -2
                                        THEN  RepeatFor  2  (D  -3)
                                        THEN  All  Reduce
                                        THEN  Thin  (-2)))
  THEN  \mforall{}h:hyp.  ((EqTypeHD  h  THENM  Thin  (h+1))  THENA  Auto)  )

---

Home Index