Step
*
2
2
2
of Lemma
simple-loc-comb-3-concat-es-sv
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. F : Id ─→ A ─→ B ─→ C ─→ bag(Top)
7. X : EClass(A)
8. Y : EClass(B)
9. Z : EClass(C)
10. ∀i:Id. ∀a:A. ∀b:B. ∀c:C. (#(F i a b c) ≤ 1)
11. ∀e:E. (#(X es e) ≤ 1)
12. ∀e:E. (#(Y es e) ≤ 1)
13. ∀e:E. (#(Z es e) ≤ 1)
14. e : E@i
15. #(X es e) ≤ 1
16. #(X es e) = 1 ∈ ℤ
17. single-valued-bag(X es e;A)
18. X es e ~ {only(X es e)}
19. #(Y es e) ≤ 1
20. #(Y es e) = 1 ∈ ℤ
21. single-valued-bag(Y es e;B)
22. Y es e ~ {only(Y es e)}
23. #(Z es e) ≤ 1
24. #(Z es e) = 1 ∈ ℤ
⊢ #(bag-union(∪x@1∈Z es e.{F loc(e) only(X es e) only(Y es e) x@1})) ≤ 1
BY
{ ((Assert single-valued-bag(Z es e;C) BY
(BLemma `single-valued-bag-if-le1` THEN Auto))⋅
THEN (FLemma `bag-size-one` [-2] THENA Auto)
THEN HypSubst' (-1) 0
THEN (RWO "bag-combine-single-left" 0 THENA Auto)
THEN (InstHyp [⌈loc(e)⌉;⌈only(X es e)⌉;⌈only(Y es e)⌉;⌈only(Z es e)⌉] (-17)⋅ THENA Auto)
THEN (Assert ⌈(#(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 0 ∈ ℤ)
∨ (#(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 1 ∈ ℤ)⌉⋅
THENA Auto'
)
THEN D (-1)) }
1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. F : Id ─→ A ─→ B ─→ C ─→ bag(Top)
7. X : EClass(A)
8. Y : EClass(B)
9. Z : EClass(C)
10. ∀i:Id. ∀a:A. ∀b:B. ∀c:C. (#(F i a b c) ≤ 1)
11. ∀e:E. (#(X es e) ≤ 1)
12. ∀e:E. (#(Y es e) ≤ 1)
13. ∀e:E. (#(Z es e) ≤ 1)
14. e : E@i
15. #(X es e) ≤ 1
16. #(X es e) = 1 ∈ ℤ
17. single-valued-bag(X es e;A)
18. X es e ~ {only(X es e)}
19. #(Y es e) ≤ 1
20. #(Y es e) = 1 ∈ ℤ
21. single-valued-bag(Y es e;B)
22. Y es e ~ {only(Y es e)}
23. #(Z es e) ≤ 1
24. #(Z es e) = 1 ∈ ℤ
25. single-valued-bag(Z es e;C)
26. Z es e ~ {only(Z es e)}
27. #(F loc(e) only(X es e) only(Y es e) only(Z es e)) ≤ 1
28. #(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 0 ∈ ℤ
⊢ #(bag-union({F loc(e) only(X es e) only(Y es e) only(Z es e)})) ≤ 1
2
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. F : Id ─→ A ─→ B ─→ C ─→ bag(Top)
7. X : EClass(A)
8. Y : EClass(B)
9. Z : EClass(C)
10. ∀i:Id. ∀a:A. ∀b:B. ∀c:C. (#(F i a b c) ≤ 1)
11. ∀e:E. (#(X es e) ≤ 1)
12. ∀e:E. (#(Y es e) ≤ 1)
13. ∀e:E. (#(Z es e) ≤ 1)
14. e : E@i
15. #(X es e) ≤ 1
16. #(X es e) = 1 ∈ ℤ
17. single-valued-bag(X es e;A)
18. X es e ~ {only(X es e)}
19. #(Y es e) ≤ 1
20. #(Y es e) = 1 ∈ ℤ
21. single-valued-bag(Y es e;B)
22. Y es e ~ {only(Y es e)}
23. #(Z es e) ≤ 1
24. #(Z es e) = 1 ∈ ℤ
25. single-valued-bag(Z es e;C)
26. Z es e ~ {only(Z es e)}
27. #(F loc(e) only(X es e) only(Y es e) only(Z es e)) ≤ 1
28. #(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 1 ∈ ℤ
⊢ #(bag-union({F loc(e) only(X es e) only(Y es e) only(Z es e)})) ≤ 1
Latex:
Latex:
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. F : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C {}\mrightarrow{} bag(Top)
7. X : EClass(A)
8. Y : EClass(B)
9. Z : EClass(C)
10. \mforall{}i:Id. \mforall{}a:A. \mforall{}b:B. \mforall{}c:C. (\#(F i a b c) \mleq{} 1)
11. \mforall{}e:E. (\#(X es e) \mleq{} 1)
12. \mforall{}e:E. (\#(Y es e) \mleq{} 1)
13. \mforall{}e:E. (\#(Z es e) \mleq{} 1)
14. e : E@i
15. \#(X es e) \mleq{} 1
16. \#(X es e) = 1
17. single-valued-bag(X es e;A)
18. X es e \msim{} \{only(X es e)\}
19. \#(Y es e) \mleq{} 1
20. \#(Y es e) = 1
21. single-valued-bag(Y es e;B)
22. Y es e \msim{} \{only(Y es e)\}
23. \#(Z es e) \mleq{} 1
24. \#(Z es e) = 1
\mvdash{} \#(bag-union(\mcup{}x@1\mmember{}Z es e.\{F loc(e) only(X es e) only(Y es e) x@1\})) \mleq{} 1
By
Latex:
((Assert single-valued-bag(Z es e;C) BY
(BLemma `single-valued-bag-if-le1` THEN Auto))\mcdot{}
THEN (FLemma `bag-size-one` [-2] THENA Auto)
THEN HypSubst' (-1) 0
THEN (RWO "bag-combine-single-left" 0 THENA Auto)
THEN (InstHyp [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}only(X es e)\mkleeneclose{};\mkleeneopen{}only(Y es e)\mkleeneclose{};\mkleeneopen{}only(Z es e)\mkleeneclose{}] (-17)\mcdot{} THENA Auto)
THEN (Assert \mkleeneopen{}(\#(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 0)
\mvee{} (\#(F loc(e) only(X es e) only(Y es e) only(Z es e)) = 1)\mkleeneclose{}\mcdot{}
THENA Auto'
)
THEN D (-1))
Home
Index