---

Step * 1 of Lemma accum_split_wf


1. A : Type
2. T : Type
3. f : (T List × A) ⟶ 𝔹
4. g : (T List × A) ⟶ A
5. x : A
6. n : ℕ
7. L : T List
8. ∀L1:T List
     (||L1|| < ||L||
     ⇒ (accum_split(g;x;f;L1) ∈ {p:(T List × A) List × T List × A| 
                                  let LL,L2 = p 
                                  in is_accum_splitting(T;A;L1;LL;L2;f;g;x)} ))
9. ↑null(L)
⊢ accum_split(g;x;f;L) ∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;L;LL;L2;f;g;x)} 
BY
{ (DVar `L'
   THEN All Reduce
   THEN Auto
   THEN RepUR ``accum_split`` 0
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``is_accum_splitting`` 0
   THEN (Auto THEN Try (BLemma `l_all_nil`) THEN Auto)
   THEN RWO  "iseg_nil" (-2)
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  x  :  A
6.  n  :  \mBbbN{}
7.  L  :  T  List
8.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\mRightarrow{}  (accum\_split(g;x;f;L1)  \mmember{}  \{p:(T  List  \mtimes{}  A)  List  \mtimes{}  T  List  \mtimes{}  A| 
                                                                    let  LL,L2  =  p 
                                                                    in  is\_accum\_splitting(T;A;L1;LL;L2;f;g;x)\}  ))
9.  \muparrow{}null(L)
\mvdash{}  accum\_split(g;x;f;L)  \mmember{}  \{p:(T  List  \mtimes{}  A)  List  \mtimes{}  T  List  \mtimes{}  A| 
                                                    let  LL,L2  =  p 
                                                    in  is\_accum\_splitting(T;A;L;LL;L2;f;g;x)\} 


By

---

Latex:
(DVar  `L'
  THEN  All  Reduce
  THEN  Auto
  THEN  RepUR  ``accum\_split``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``is\_accum\_splitting``  0
  THEN  (Auto  THEN  Try  (BLemma  `l\_all\_nil`)  THEN  Auto)
  THEN  RWO    "iseg\_nil"  (-2)
  THEN  Auto)

---

Home Index