---

Step * 2 2 1 1 4 of Lemma list_split_wf


1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ¬↑(f [u / v])
14. (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1) @ [u / (v @ [last(L)])]) ∈ (T List)
15. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
16. (¬↑null(firstn(||L|| - 1;L) @ [last(L)])) ⇒ (¬False)
17. S : T List
18. ¬↑null(S)
19. S ≤ [u / (v @ [last(L)])]
20. ¬(S = [u / (v @ [last(L)])] ∈ (T List))
⊢ ¬↑(f S)
BY
{ ((D 0 THENA Auto) THEN InstHyp [⌜S⌝] 12⋅ THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ¬↑null(L)
6. v1 : T List List
7. u : T
8. v : T List
9. firstn(||L|| - 1;L) = (concat(v1) @ [u / v]) ∈ (T List)
10. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
11. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬False)
12. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ [u / v] ⇒ (¬(S = [u / v] ∈ (T List))) ⇒ (¬↑(f S)))
13. ¬↑(f [u / v])
14. (firstn(||L|| - 1;L) @ [last(L)]) = (concat(v1) @ [u / (v @ [last(L)])]) ∈ (T List)
15. (∀L'∈v1.(↑(f L')) ∧ (¬↑null(L')) ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ L' ⇒ (¬(S = L' ∈ (T List))) ⇒ (¬↑(f S)))))
16. (¬↑null(firstn(||L|| - 1;L) @ [last(L)])) ⇒ (¬False)
17. S : T List
18. ¬↑null(S)
19. S ≤ [u / (v @ [last(L)])]
20. ¬(S = [u / (v @ [last(L)])] ∈ (T List))
21. ↑(f S)
⊢ S ≤ [u / v]

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  n  :  \mBbbN{}
4.  L  :  T  List
5.  \mneg{}\muparrow{}null(L)
6.  v1  :  T  List  List
7.  u  :  T
8.  v  :  T  List
9.  firstn(||L||  -  1;L)  =  (concat(v1)  @  [u  /  v])
10.  (\mforall{}L'\mmember{}v1.(\muparrow{}(f  L'))
                \mwedge{}  (\mneg{}\muparrow{}null(L'))
                \mwedge{}  (\mforall{}S:T  List.  ((\mneg{}\muparrow{}null(S))  {}\mRightarrow{}  S  \mleq{}  L'  {}\mRightarrow{}  (\mneg{}(S  =  L'))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  S)))))
11.  (\mneg{}\muparrow{}null(firstn(||L||  -  1;L)))  {}\mRightarrow{}  (\mneg{}False)
12.  \mforall{}S:T  List.  ((\mneg{}\muparrow{}null(S))  {}\mRightarrow{}  S  \mleq{}  [u  /  v]  {}\mRightarrow{}  (\mneg{}(S  =  [u  /  v]))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  S)))
13.  \mneg{}\muparrow{}(f  [u  /  v])
14.  (firstn(||L||  -  1;L)  @  [last(L)])  =  (concat(v1)  @  [u  /  (v  @  [last(L)])])
15.  (\mforall{}L'\mmember{}v1.(\muparrow{}(f  L'))
                \mwedge{}  (\mneg{}\muparrow{}null(L'))
                \mwedge{}  (\mforall{}S:T  List.  ((\mneg{}\muparrow{}null(S))  {}\mRightarrow{}  S  \mleq{}  L'  {}\mRightarrow{}  (\mneg{}(S  =  L'))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  S)))))
16.  (\mneg{}\muparrow{}null(firstn(||L||  -  1;L)  @  [last(L)]))  {}\mRightarrow{}  (\mneg{}False)
17.  S  :  T  List
18.  \mneg{}\muparrow{}null(S)
19.  S  \mleq{}  [u  /  (v  @  [last(L)])]
20.  \mneg{}(S  =  [u  /  (v  @  [last(L)])])
\mvdash{}  \mneg{}\muparrow{}(f  S)


By

---

Latex:
((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}S\mkleeneclose{}]  12\mcdot{}  THEN  Auto)

---

Home Index