---

Step * 1 2 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. y : Unit@i
9. ∀cs:bag(X). (¬(b1 = (b + cs) ∈ bag(X)))
10. b1 = (b + c) ∈ bag(X)
⊢ 0 = 1 ∈ |r|
BY
{ TACTIC:(InstHyp [⌜c⌝] (-2)⋅ 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.  y  :  Unit@i
9.  \mforall{}cs:bag(X).  (\mneg{}(b1  =  (b  +  cs)))
10.  b1  =  (b  +  c)
\mvdash{}  0  =  1


By

---

Latex:
TACTIC:(InstHyp  [\mkleeneopen{}c\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index