Step
*
1
1
1
3
2
1
of Lemma
Accum-class-progress
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. P : A ⟶ B ⟶ ℙ@i'
6. f : A ⟶ B ⟶ B@i
7. init : Id ⟶ bag(B)@i
8. X : EClass(A)@i'
9. es : EO+(Info)@i'
10. e1 : E@i
11. e2 : E@i
12. ∀e':E
((e' < e2)
⇒ (∀v1,v2:B.
((∀a:A. ∀s:B. Dec(P[a;s]))
⇒ Trans(B;x,y.R[x;y])
⇒ (∀s1,s2:B. SqStable(R[s1;s2]))
⇒ (∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
⇒ single-valued-classrel(es;X;A)
⇒ single-valued-bag(init loc(e1);B)
⇒ v1 ∈ Accum-class(f;init;X)(e1)
⇒ v2 ∈ Accum-class(f;init;X)(e')
⇒ (e1 <loc e')
⇒ (((∃e:E
∃a:A
∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;v2])
∧ ((∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = v2 ∈ B))))))
13. v1 : B@i
14. v2 : B@i
15. ∀a:A. ∀s:B. Dec(P[a;s])@i
16. Trans(B;x,y.R[x;y])@i
17. ∀s1,s2:B. SqStable(R[s1;s2])@i
18. ∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e2
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B))))@i
19. single-valued-classrel(es;X;A)@i
20. single-valued-bag(init loc(e1);B)@i
21. v1 ∈ Accum-class(f;init;X)(e1)@i
22. a : A
23. b : B
24. v2 = (f a b) ∈ B
25. e' : E
26. (e' <loc e2)
27. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
28. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
29. b ∈ Accum-class(f;init;X)(e')
30. a ∈ X(e2)
31. (e1 <loc e2)@i
32. b ∈ Prior(Accum-class(f;init;X))?init(e2)
33. (e1 <loc e')
34. (∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;b]
35. (∀e:E. ∀s:B.
((e1 <loc e) ⇒ e ≤loc e' ⇒ s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = b ∈ B)
36. e : E@i
37. a1 : A@i
38. s : B@i
39. (e1 <loc e)@i
40. e = e2 ∈ E@i
41. s ∈ Prior(Accum-class(f;init;X))?init(e)@i
42. a1 ∈ X(e2)
43. P[a1;s]@i
44. (e' <loc e)
45. a = a1 ∈ A
46. b = s ∈ B
47. (¬P[a;b]) ⇒ (b = (f a b) ∈ B)
48. R[b;f a b]
⊢ R[v1;v2]
BY
{ (InstLemma `decidable__existse-between3` [⌜es⌝;⌜e1⌝;⌜e'⌝;⌜λe.∃a:A
∃s:B
(s ∈ Prior(Accum-class(f;init;X))?init(e)
∧ a ∈ X(e)
∧ P[a;s])⌝]⋅
THENA (Auto THEN RepUR ``alle-at so_apply`` 0 THEN Auto)
) }
1
.....decidable?.....
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. P : A ⟶ B ⟶ ℙ@i'
6. f : A ⟶ B ⟶ B@i
7. init : Id ⟶ bag(B)@i
8. X : EClass(A)@i'
9. es : EO+(Info)@i'
10. e1 : E@i
11. e2 : E@i
12. ∀e':E
((e' < e2)
⇒ (∀v1,v2:B.
((∀a:A. ∀s:B. Dec(P[a;s]))
⇒ Trans(B;x,y.R[x;y])
⇒ (∀s1,s2:B. SqStable(R[s1;s2]))
⇒ (∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
⇒ single-valued-classrel(es;X;A)
⇒ single-valued-bag(init loc(e1);B)
⇒ v1 ∈ Accum-class(f;init;X)(e1)
⇒ v2 ∈ Accum-class(f;init;X)(e')
⇒ (e1 <loc e')
⇒ (((∃e:E
∃a:A
∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;v2])
∧ ((∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = v2 ∈ B))))))
13. v1 : B@i
14. v2 : B@i
15. ∀a:A. ∀s:B. Dec(P[a;s])@i
16. Trans(B;x,y.R[x;y])@i
17. ∀s1,s2:B. SqStable(R[s1;s2])@i
18. ∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e2
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B))))@i
19. single-valued-classrel(es;X;A)@i
20. single-valued-bag(init loc(e1);B)@i
21. v1 ∈ Accum-class(f;init;X)(e1)@i
22. a : A
23. b : B
24. v2 = (f a b) ∈ B
25. e' : E
26. (e' <loc e2)
27. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
28. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
29. b ∈ Accum-class(f;init;X)(e')
30. a ∈ X(e2)
31. (e1 <loc e2)@i
32. b ∈ Prior(Accum-class(f;init;X))?init(e2)
33. (e1 <loc e')
34. (∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;b]
35. (∀e:E. ∀s:B.
((e1 <loc e) ⇒ e ≤loc e' ⇒ s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = b ∈ B)
36. e : E@i
37. a1 : A@i
38. s : B@i
39. (e1 <loc e)@i
40. e = e2 ∈ E@i
41. s ∈ Prior(Accum-class(f;init;X))?init(e)@i
42. a1 ∈ X(e2)
43. P[a1;s]@i
44. (e' <loc e)
45. a = a1 ∈ A
46. b = s ∈ B
47. (¬P[a;b]) ⇒ (b = (f a b) ∈ B)
48. R[b;f a b]
49. e3 : E@i
50. loc(e3) = loc(e1) ∈ Id@i
51. ¬↑first(e3)
⊢ Dec(∃a:A. ∃s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e3) ∧ a ∈ X(e3) ∧ (P a s)))
2
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. P : A ⟶ B ⟶ ℙ@i'
6. f : A ⟶ B ⟶ B@i
7. init : Id ⟶ bag(B)@i
8. X : EClass(A)@i'
9. es : EO+(Info)@i'
10. e1 : E@i
11. e2 : E@i
12. ∀e':E
((e' < e2)
⇒ (∀v1,v2:B.
((∀a:A. ∀s:B. Dec(P[a;s]))
⇒ Trans(B;x,y.R[x;y])
⇒ (∀s1,s2:B. SqStable(R[s1;s2]))
⇒ (∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
⇒ single-valued-classrel(es;X;A)
⇒ single-valued-bag(init loc(e1);B)
⇒ v1 ∈ Accum-class(f;init;X)(e1)
⇒ v2 ∈ Accum-class(f;init;X)(e')
⇒ (e1 <loc e')
⇒ (((∃e:E
∃a:A
∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;v2])
∧ ((∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e'
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = v2 ∈ B))))))
13. v1 : B@i
14. v2 : B@i
15. ∀a:A. ∀s:B. Dec(P[a;s])@i
16. Trans(B;x,y.R[x;y])@i
17. ∀s1,s2:B. SqStable(R[s1;s2])@i
18. ∀a:A. ∀e:E. ∀s:B.
((e1 <loc e)
⇒ e ≤loc e2
⇒ a ∈ X(e)
⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B))))@i
19. single-valued-classrel(es;X;A)@i
20. single-valued-bag(init loc(e1);B)@i
21. v1 ∈ Accum-class(f;init;X)(e1)@i
22. a : A
23. b : B
24. v2 = (f a b) ∈ B
25. e' : E
26. (e' <loc e2)
27. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
28. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
29. b ∈ Accum-class(f;init;X)(e')
30. a ∈ X(e2)
31. (e1 <loc e2)@i
32. b ∈ Prior(Accum-class(f;init;X))?init(e2)
33. (e1 <loc e')
34. (∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e' ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
⇒ R[v1;b]
35. (∀e:E. ∀s:B.
((e1 <loc e) ⇒ e ≤loc e' ⇒ s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
⇒ (v1 = b ∈ B)
36. e : E@i
37. a1 : A@i
38. s : B@i
39. (e1 <loc e)@i
40. e = e2 ∈ E@i
41. s ∈ Prior(Accum-class(f;init;X))?init(e)@i
42. a1 ∈ X(e2)
43. P[a1;s]@i
44. (e' <loc e)
45. a = a1 ∈ A
46. b = s ∈ B
47. (¬P[a;b]) ⇒ (b = (f a b) ∈ B)
48. R[b;f a b]
49. Dec(∃e∈(e1,e'].λe.∃a:A. ∃s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s])[e])
⊢ R[v1;v2]
Latex:
Latex:
1. Info : Type
2. B : Type
3. A : Type
4. R : B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}@i'
5. P : A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}@i'
6. f : A {}\mrightarrow{} B {}\mrightarrow{} B@i
7. init : Id {}\mrightarrow{} bag(B)@i
8. X : EClass(A)@i'
9. es : EO+(Info)@i'
10. e1 : E@i
11. e2 : E@i
12. \mforall{}e':E
((e' < e2)
{}\mRightarrow{} (\mforall{}v1,v2:B.
((\mforall{}a:A. \mforall{}s:B. Dec(P[a;s]))
{}\mRightarrow{} Trans(B;x,y.R[x;y])
{}\mRightarrow{} (\mforall{}s1,s2:B. SqStable(R[s1;s2]))
{}\mRightarrow{} (\mforall{}a:A. \mforall{}e:E. \mforall{}s:B.
((e1 <loc e)
{}\mRightarrow{} e \mleq{}loc e'
{}\mRightarrow{} a \mmember{} X(e)
{}\mRightarrow{} s \mmember{} Prior(Accum-class(f;init;X))?init(e)
{}\mRightarrow{} ((P[a;s] {}\mRightarrow{} R[s;f a s]) \mwedge{} ((\mneg{}P[a;s]) {}\mRightarrow{} (s = (f a s))))))
{}\mRightarrow{} single-valued-classrel(es;X;A)
{}\mRightarrow{} single-valued-bag(init loc(e1);B)
{}\mRightarrow{} v1 \mmember{} Accum-class(f;init;X)(e1)
{}\mRightarrow{} v2 \mmember{} Accum-class(f;init;X)(e')
{}\mRightarrow{} (e1 <loc e')
{}\mRightarrow{} (((\mexists{}e:E
\mexists{}a:A
\mexists{}s:B
((e1 <loc e)
\mwedge{} e \mleq{}loc e'
\mwedge{} s \mmember{} Prior(Accum-class(f;init;X))?init(e)
\mwedge{} a \mmember{} X(e)
\mwedge{} P[a;s]))
{}\mRightarrow{} R[v1;v2])
\mwedge{} ((\mforall{}e:E. \mforall{}s:B.
((e1 <loc e)
{}\mRightarrow{} e \mleq{}loc e'
{}\mRightarrow{} s \mmember{} Prior(Accum-class(f;init;X))?init(e)
{}\mRightarrow{} (\mforall{}a:A. ((\mneg{}a \mmember{} X(e)) \mvee{} (\mneg{}P[a;s])))))
{}\mRightarrow{} (v1 = v2))))))
13. v1 : B@i
14. v2 : B@i
15. \mforall{}a:A. \mforall{}s:B. Dec(P[a;s])@i
16. Trans(B;x,y.R[x;y])@i
17. \mforall{}s1,s2:B. SqStable(R[s1;s2])@i
18. \mforall{}a:A. \mforall{}e:E. \mforall{}s:B.
((e1 <loc e)
{}\mRightarrow{} e \mleq{}loc e2
{}\mRightarrow{} a \mmember{} X(e)
{}\mRightarrow{} s \mmember{} Prior(Accum-class(f;init;X))?init(e)
{}\mRightarrow{} ((P[a;s] {}\mRightarrow{} R[s;f a s]) \mwedge{} ((\mneg{}P[a;s]) {}\mRightarrow{} (s = (f a s)))))@i
19. single-valued-classrel(es;X;A)@i
20. single-valued-bag(init loc(e1);B)@i
21. v1 \mmember{} Accum-class(f;init;X)(e1)@i
22. a : A
23. b : B
24. v2 = (f a b)
25. e' : E
26. (e' <loc e2)
27. \mdownarrow{}\mexists{}w:B. w \mmember{} Accum-class(f;init;X)(e')
28. \mforall{}e'':E. ((e'' <loc e2) {}\mRightarrow{} (e' <loc e'') {}\mRightarrow{} (\mneg{}\mdownarrow{}\mexists{}w:B. w \mmember{} Accum-class(f;init;X)(e'')))
29. b \mmember{} Accum-class(f;init;X)(e')
30. a \mmember{} X(e2)
31. (e1 <loc e2)@i
32. b \mmember{} Prior(Accum-class(f;init;X))?init(e2)
33. (e1 <loc e')
34. (\mexists{}e:E
\mexists{}a:A
\mexists{}s:B
((e1 <loc e) \mwedge{} e \mleq{}loc e' \mwedge{} s \mmember{} Prior(Accum-class(f;init;X))?init(e) \mwedge{} a \mmember{} X(e) \mwedge{} P[a;s]))
{}\mRightarrow{} R[v1;b]
35. (\mforall{}e:E. \mforall{}s:B.
((e1 <loc e)
{}\mRightarrow{} e \mleq{}loc e'
{}\mRightarrow{} s \mmember{} Prior(Accum-class(f;init;X))?init(e)
{}\mRightarrow{} (\mforall{}a:A. ((\mneg{}a \mmember{} X(e)) \mvee{} (\mneg{}P[a;s])))))
{}\mRightarrow{} (v1 = b)
36. e : E@i
37. a1 : A@i
38. s : B@i
39. (e1 <loc e)@i
40. e = e2@i
41. s \mmember{} Prior(Accum-class(f;init;X))?init(e)@i
42. a1 \mmember{} X(e2)
43. P[a1;s]@i
44. (e' <loc e)
45. a = a1
46. b = s
47. (\mneg{}P[a;b]) {}\mRightarrow{} (b = (f a b))
48. R[b;f a b]
\mvdash{} R[v1;v2]
By
Latex:
(InstLemma `decidable\_\_existse-between3` [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}\mlambda{}e.\mexists{}a:A
\mexists{}s:B
(s \mmember{}
Prior(Accum-class(f;init;X))?init(
e)
\mwedge{} a \mmember{} X(e)
\mwedge{} P[a;s])\mkleeneclose{}]\mcdot{}
THENA (Auto THEN RepUR ``alle-at so\_apply`` 0 THEN Auto)
)
Home
Index