Step
*
2
2
1
of Lemma
simple-loc-comb-3-concat-single-val
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. D : Type
7. F : Id ─→ A ─→ B ─→ C ─→ bag(D)
8. X : EClass(A)
9. Y : EClass(B)
10. Z : EClass(C)
11. ∀i:Id. ∀a:A. ∀b:B. ∀c:C. (#(F i a b c) ≤ 1)
12. ∀e:E. ∀v1,v2:A. (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ A))
13. ∀e:E. ∀v1,v2:B. (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))
14. ∀e:E. ∀v1,v2:C. (v1 ∈ Z(e) ⇒ v2 ∈ Z(e) ⇒ (v1 = v2 ∈ C))
15. e : E@i
16. v1 : D@i
17. v2 : D@i
18. b : bag(D)
19. v1 ↓∈ b
20. x : A
21. x ↓∈ X es e
22. x@0 : B
23. x@0 ↓∈ Y es e
24. x@1 : C
25. x@1 ↓∈ Z es e
26. b = (F loc(e) x x@0 x@1) ∈ bag(D)
27. b1 : bag(D)
28. v2 ↓∈ b1
29. x1 : A
30. x1 ↓∈ X es e
31. x2 : B
32. x2 ↓∈ Y es e
33. x3 : C
34. x3 ↓∈ Z es e
35. b1 = (F loc(e) x1 x2 x3) ∈ bag(D)
36. #(F loc(e) x x@0 x@1) ≤ 1
37. #(F loc(e) x1 x2 x3) ≤ 1
⊢ v1 = v2 ∈ D
BY
{ ((Assert ⌈(#(F loc(e) x x@0 x@1) ≤ 0) ∨ (#(F loc(e) x x@0 x@1) = 1 ∈ ℤ)⌉⋅ THENA MaAuto)
THEN (Assert ⌈(#(F loc(e) x1 x2 x3) ≤ 0) ∨ (#(F loc(e) x1 x2 x3) = 1 ∈ ℤ)⌉⋅ THENA MaAuto)
THEN D (-2)
THEN D (-1)
THEN Try (Complete (((FLemma `bag-size-zero` [-1] THENA Auto)
THEN (RWO "-1" (-6) THENA Auto)
THEN (RWO "-6" (-13) THENA Auto)
THEN BagMemberD (-13))))
THEN Try (Complete (((FLemma `bag-size-zero` [-2] THENA Auto)
THEN (RWO "-1" (-15) THENA Auto)
THEN (RWO "-15" (-22) THENA Auto)
THEN BagMemberD (-22))))) }
1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. D : Type
7. F : Id ─→ A ─→ B ─→ C ─→ bag(D)
8. X : EClass(A)
9. Y : EClass(B)
10. Z : EClass(C)
11. ∀i:Id. ∀a:A. ∀b:B. ∀c:C. (#(F i a b c) ≤ 1)
12. ∀e:E. ∀v1,v2:A. (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ A))
13. ∀e:E. ∀v1,v2:B. (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))
14. ∀e:E. ∀v1,v2:C. (v1 ∈ Z(e) ⇒ v2 ∈ Z(e) ⇒ (v1 = v2 ∈ C))
15. e : E@i
16. v1 : D@i
17. v2 : D@i
18. b : bag(D)
19. v1 ↓∈ b
20. x : A
21. x ↓∈ X es e
22. x@0 : B
23. x@0 ↓∈ Y es e
24. x@1 : C
25. x@1 ↓∈ Z es e
26. b = (F loc(e) x x@0 x@1) ∈ bag(D)
27. b1 : bag(D)
28. v2 ↓∈ b1
29. x1 : A
30. x1 ↓∈ X es e
31. x2 : B
32. x2 ↓∈ Y es e
33. x3 : C
34. x3 ↓∈ Z es e
35. b1 = (F loc(e) x1 x2 x3) ∈ bag(D)
36. #(F loc(e) x x@0 x@1) ≤ 1
37. #(F loc(e) x1 x2 x3) ≤ 1
38. #(F loc(e) x x@0 x@1) = 1 ∈ ℤ
39. #(F loc(e) x1 x2 x3) = 1 ∈ ℤ
⊢ v1 = v2 ∈ D
Latex:
Latex:
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. D : Type
7. F : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C {}\mrightarrow{} bag(D)
8. X : EClass(A)
9. Y : EClass(B)
10. Z : EClass(C)
11. \mforall{}i:Id. \mforall{}a:A. \mforall{}b:B. \mforall{}c:C. (\#(F i a b c) \mleq{} 1)
12. \mforall{}e:E. \mforall{}v1,v2:A. (v1 \mmember{} X(e) {}\mRightarrow{} v2 \mmember{} X(e) {}\mRightarrow{} (v1 = v2))
13. \mforall{}e:E. \mforall{}v1,v2:B. (v1 \mmember{} Y(e) {}\mRightarrow{} v2 \mmember{} Y(e) {}\mRightarrow{} (v1 = v2))
14. \mforall{}e:E. \mforall{}v1,v2:C. (v1 \mmember{} Z(e) {}\mRightarrow{} v2 \mmember{} Z(e) {}\mRightarrow{} (v1 = v2))
15. e : E@i
16. v1 : D@i
17. v2 : D@i
18. b : bag(D)
19. v1 \mdownarrow{}\mmember{} b
20. x : A
21. x \mdownarrow{}\mmember{} X es e
22. x@0 : B
23. x@0 \mdownarrow{}\mmember{} Y es e
24. x@1 : C
25. x@1 \mdownarrow{}\mmember{} Z es e
26. b = (F loc(e) x x@0 x@1)
27. b1 : bag(D)
28. v2 \mdownarrow{}\mmember{} b1
29. x1 : A
30. x1 \mdownarrow{}\mmember{} X es e
31. x2 : B
32. x2 \mdownarrow{}\mmember{} Y es e
33. x3 : C
34. x3 \mdownarrow{}\mmember{} Z es e
35. b1 = (F loc(e) x1 x2 x3)
36. \#(F loc(e) x x@0 x@1) \mleq{} 1
37. \#(F loc(e) x1 x2 x3) \mleq{} 1
\mvdash{} v1 = v2
By
Latex:
((Assert \mkleeneopen{}(\#(F loc(e) x x@0 x@1) \mleq{} 0) \mvee{} (\#(F loc(e) x x@0 x@1) = 1)\mkleeneclose{}\mcdot{} THENA MaAuto)
THEN (Assert \mkleeneopen{}(\#(F loc(e) x1 x2 x3) \mleq{} 0) \mvee{} (\#(F loc(e) x1 x2 x3) = 1)\mkleeneclose{}\mcdot{} THENA MaAuto)
THEN D (-2)
THEN D (-1)
THEN Try (Complete (((FLemma `bag-size-zero` [-1] THENA Auto)
THEN (RWO "-1" (-6) THENA Auto)
THEN (RWO "-6" (-13) THENA Auto)
THEN BagMemberD (-13))))
THEN Try (Complete (((FLemma `bag-size-zero` [-2] THENA Auto)
THEN (RWO "-1" (-15) THENA Auto)
THEN (RWO "-15" (-22) THENA Auto)
THEN BagMemberD (-22)))))
Home
Index