Step
*
2
1
1
2
of Lemma
accum_split_wf
.....falsecase.....
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))
⊢ let LL,L2 = if f <v3, v4> then <v1 @ [<v3, v4>], [last(L)], g <v3, v4>> else <v1, v3 @ [last(L)], v4> fi
in is_accum_splitting(T;A;firstn(||L|| - 1;L) @ [last(L)];LL;L2;f;g;x)
BY
{ ((SplitOnConclITE THENA Auto)
THEN Reduce 0
THEN RepUR ``is_accum_splitting`` 0
THEN SplitAndConcl
THEN Intros
THEN Try (Trivial)) }
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. ¬↑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)
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. ¬↑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>)
⊢ (∀L'∈v1 @ [<v3, v4>].(↑(f L'))
∧ (¬↑null(fst(L')))
∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
3
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>)
20. ¬↑null(firstn(||L|| - 1;L) @ [last(L)])
⊢ ¬False
4
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>)
20. S : T List
21. ¬↑null(S)
22. S ≤ [last(L)]
23. ¬(S = [last(L)] ∈ (T List))
⊢ ¬↑(f <S, g <v3, v4>>)
5
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>)
⊢ (snd(hd((v1 @ [<v3, v4>]) @ [<[last(L)], g <v3, v4>>]))) = x ∈ A
6
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>)
20. i : ℕ||v1 @ [<v3, v4>]||
⊢ (snd((v1 @ [<v3, v4>]) @ [<[last(L)], g <v3, v4>>][i + 1])) = (g v1 @ [<v3, v4>][i]) ∈ A
7
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 @ [last(L)]) ∈ (T List)
8
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>)
20. ¬↑null(firstn(||L|| - 1;L) @ [last(L)])
⊢ ¬↑null(v3 @ [last(L)])
9
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>)
20. S : T List
21. ¬↑null(S)
22. S ≤ v3 @ [last(L)]
23. ¬(S = (v3 @ [last(L)]) ∈ (T List))
⊢ ¬↑(f <S, v4>)
10
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>)
⊢ (snd(hd(v1 @ [<v3 @ [last(L)], v4>]))) = x ∈ A
11
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>)
20. i : ℕ||v1||
⊢ (snd(v1 @ [<v3 @ [last(L)], v4>][i + 1])) = (g v1[i]) ∈ A
Latex:
Latex:
.....falsecase.....
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 = [])
\mvdash{} let LL,L2 = if f <v3, v4>
then <v1 @ [<v3, v4>], [last(L)], g <v3, v4>>
else <v1, v3 @ [last(L)], v4>
fi
in is\_accum\_splitting(T;A;firstn(||L|| - 1;L) @ [last(L)];LL;L2;f;g;x)
By
Latex:
((SplitOnConclITE THENA Auto)
THEN Reduce 0
THEN RepUR ``is\_accum\_splitting`` 0
THEN SplitAndConcl
THEN Intros
THEN Try (Trivial))
Home
Index