---

Step * 2 1 1 2 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. ¬↑null(L)
9. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. firstn(||L|| - 1;L) = (concat(map(λp.(fst(p));v1)) @ v3) ∈ (T List)
13. (∀L'∈v1.(↑(f L'))
        ∧ (¬↑null(fst(L')))
        ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
14. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬↑null(v3))
15. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ v3 ⇒ (¬(S = v3 ∈ (T List))) ⇒ (¬↑(f <S, v4>)))
16. (snd(hd(v1 @ [<v3, v4>]))) = x ∈ A
17. ∀i:ℕ||v1||. ((snd(v1 @ [<v3, v4>][i + 1])) = (g v1[i]) ∈ A)
18. ¬(v3 = [] ∈ (T List))
19. ↑(f <v3, v4>)
⊢ (firstn(||L|| - 1;L) @ [last(L)]) = (concat(map(λp.(fst(p));v1 @ [<v3, v4>])) @ [last(L)]) ∈ (T List)
BY
{ EqCDA }

1
.....subterm..... T:t
1:n
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. ¬↑null(L)
9. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. firstn(||L|| - 1;L) = (concat(map(λp.(fst(p));v1)) @ v3) ∈ (T List)
13. (∀L'∈v1.(↑(f L'))
        ∧ (¬↑null(fst(L')))
        ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
14. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬↑null(v3))
15. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ v3 ⇒ (¬(S = v3 ∈ (T List))) ⇒ (¬↑(f <S, v4>)))
16. (snd(hd(v1 @ [<v3, v4>]))) = x ∈ A
17. ∀i:ℕ||v1||. ((snd(v1 @ [<v3, v4>][i + 1])) = (g v1[i]) ∈ A)
18. ¬(v3 = [] ∈ (T List))
19. ↑(f <v3, v4>)
⊢ firstn(||L|| - 1;L) = concat(map(λp.(fst(p));v1 @ [<v3, v4>])) ∈ (T List)

---

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.  \mneg{}\muparrow{}null(L)
9.  v1  :  (T  List  \mtimes{}  A)  List
10.  v3  :  T  List
11.  v4  :  A
12.  firstn(||L||  -  1;L)  =  (concat(map(\mlambda{}p.(fst(p));v1))  @  v3)
13.  (\mforall{}L'\mmember{}v1.(\muparrow{}(f  L'))
                \mwedge{}  (\mneg{}\muparrow{}null(fst(L')))
                \mwedge{}  (\mforall{}S:T  List.  ((\mneg{}\muparrow{}null(S))  {}\mRightarrow{}  S  \mleq{}  fst(L')  {}\mRightarrow{}  (\mneg{}(S  =  (fst(L'))))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  <S,  snd(L')>)))))
14.  (\mneg{}\muparrow{}null(firstn(||L||  -  1;L)))  {}\mRightarrow{}  (\mneg{}\muparrow{}null(v3))
15.  \mforall{}S:T  List.  ((\mneg{}\muparrow{}null(S))  {}\mRightarrow{}  S  \mleq{}  v3  {}\mRightarrow{}  (\mneg{}(S  =  v3))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  <S,  v4>)))
16.  (snd(hd(v1  @  [<v3,  v4>])))  =  x
17.  \mforall{}i:\mBbbN{}||v1||.  ((snd(v1  @  [<v3,  v4>][i  +  1]))  =  (g  v1[i]))
18.  \mneg{}(v3  =  [])
19.  \muparrow{}(f  <v3,  v4>)
\mvdash{}  (firstn(||L||  -  1;L)  @  [last(L)])  =  (concat(map(\mlambda{}p.(fst(p));v1  @  [<v3,  v4>]))  @  [last(L)])


By

---

Latex:
EqCDA

---

Home Index