---

Step * 2 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
{ (Subst ⌜L ~ firstn(||L|| - 1;L) @ [last(L)]⌝ 0⋅
   THENL [(BLemma `last-lemma-sq`  THEN Auto)
         ; (InstHyp [⌜firstn(||L|| - 1;L)⌝] (-2)⋅
            THENA (Auto THEN RWO "length_firstn" 0 THEN Auto THEN DVar `L' THEN All Reduce THEN Auto')
            )]
) }

1
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)
10. accum_split(g;x;f;firstn(||L|| - 1;L)) ∈ {p:(T List × A) List × T List × A| 
                                              let LL,L2 = p 
                                              in is_accum_splitting(T;A;firstn(||L|| - 1;L);LL;L2;f;g;x)} 
⊢ accum_split(g;x;f;firstn(||L|| - 1;L) @ [last(L)]) ∈ {p:(T List × A) List × T List × A| 
                                                        let LL,L2 = p 
                                                        in is_accum_splitting(T;A;firstn(||L|| - 1;L)
                                                           @ [last(L)];LL;L2;f;g;x)} 

---

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.  \mneg{}\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:
(Subst  \mkleeneopen{}L  \msim{}  firstn(||L||  -  1;L)  @  [last(L)]\mkleeneclose{}  0\mcdot{}
  THENL  [(BLemma  `last-lemma-sq`    THEN  Auto)
              ;  (InstHyp  [\mkleeneopen{}firstn(||L||  -  1;L)\mkleeneclose{}]  (-2)\mcdot{}
                    THENA  (Auto  THEN  RWO  "length\_firstn"  0  THEN  Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto')
                    )]
)

---

Home Index