---

Step * of Lemma accum_split_wf

No Annotations
∀[A,T:Type]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[g:(T List × A) ⟶ A]. ∀[x:A]. ∀[L:T List].
  (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
{ (InductionOnLength THEN (Decide ↑null(L) THENA 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)
⊢ 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)} 

2
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)} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,T:Type].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].  \mforall{}[x:A].  \mforall{}[L:T  List].
    (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:
(InductionOnLength  THEN  (Decide  \muparrow{}null(L)  THENA  Auto))

---

Home Index