---

Step * 1 1 of Lemma fps-mul-single


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. b : bag(X)
6. c : bag(X)
7. b1 : bag(X)@i
8. x : bag(X)@i
9. ¬(x = c ∈ bag(X))
10. b1 = (b + x) ∈ bag(X)
11. b1 = (b + c) ∈ bag(X)
⊢ 0 = 1 ∈ |r|
BY
{ TACTIC:((Assert ⌜(b + c) = (b + x) ∈ bag(X)⌝⋅ THEN Auto) THEN RWO "bag-append-cancel" (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  b  :  bag(X)
6.  c  :  bag(X)
7.  b1  :  bag(X)@i
8.  x  :  bag(X)@i
9.  \mneg{}(x  =  c)
10.  b1  =  (b  +  x)
11.  b1  =  (b  +  c)
\mvdash{}  0  =  1


By

---

Latex:
TACTIC:((Assert  \mkleeneopen{}(b  +  c)  =  (b  +  x)\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  RWO  "bag-append-cancel"  (-1)  THEN  Auto)\mcdot{}

---

Home Index