---

Step * 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
⊢ case bag-diff(eq;b1;b) of inl(d) => if bag-eq(eq;d;c) then 1 else 0 fi  | inr(z) => 0
= if bag-eq(eq;b1;b + c) then 1 else 0 fi 
∈ |r|
BY
{ TACTIC:((InstLemma `bag-diff-property` [⌜X⌝;⌜eq⌝;⌜b⌝;⌜b1⌝]⋅ THEN Auto)
          THEN MoveToConcl (-1)
          THEN GenConclAtAddr [1;1]
          THEN Thin (-1)
          THEN D -1
          THEN Reduce 0
          THEN Auto
          THEN Repeat (AutoSplit)) }

1
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|

2
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|

---

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
\mvdash{}  case  bag-diff(eq;b1;b)  of  inl(d)  =>  if  bag-eq(eq;d;c)  then  1  else  0  fi    |  inr(z)  =>  0
=  if  bag-eq(eq;b1;b  +  c)  then  1  else  0  fi 


By

---

Latex:
TACTIC:((InstLemma  `bag-diff-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  MoveToConcl  (-1)
                THEN  GenConclAtAddr  [1;1]
                THEN  Thin  (-1)
                THEN  D  -1
                THEN  Reduce  0
                THEN  Auto
                THEN  Repeat  (AutoSplit))

---

Home Index