---

Step * 1 of Lemma accum_split_iseg2


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))
BY
{ (MoveToConcl 9
   THEN (At Type (HypSubst' (-2) 0)⋅
         THENA ((Auto THEN GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0 THEN Auto) THEN Reduce 0)
         )
   THEN (At Type (HypSubst' (-1) 0) THENA (Auto THEN GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0 THEN Auto))
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  x  :  A
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
6.  L1  :  T  List
7.  L2  :  T  List
8.  L1  \mleq{}  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)  \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))
10.  LL1  :  (T  List  \mtimes{}  A)  List
11.  LL2  :  (T  List  \mtimes{}  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>
17.  accum\_split(g;x;f;L2)  =  <LL2,  Y,  z2>
\mvdash{}  ((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:
(MoveToConcl  9
  THEN  (At  Type  (HypSubst'  (-2)  0)\mcdot{}
              THENA  ((Auto  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)  THEN  Reduce  0)
              )
  THEN  (At  Type  (HypSubst'  (-1)  0)
              THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)
              )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index