---

Step * of Lemma fps-set-to-one-single

∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ]. ∀[b:bag(Atom)].
  ([<b>]_n(y:=1) = if (#(b) =z n) then <(b|¬y)> else 0 fi  ∈ PowerSeries(r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN (InstLemma `bag-restrict-split` [⌜Atom⌝;⌜AtomDeq⌝;⌜y⌝;⌜b⌝]⋅ THENA Auto)
   THEN RepUR ``fps-zero fps-single fps-coeff fps-set-to-one`` 0
   THEN RepeatFor 3 (AutoSplit)
   THEN Try (((RWO "eqtt_to_assert eqff_to_assert" (-1) THENA Auto) THEN RW assert_pushdownC (-1) THEN Auto'))) }

1
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. b1 : bag(Atom)
6. b = ((b|y) + (b|¬y)) ∈ bag(Atom)
7. 0 < (#y in b1)
8. #(b) = n ∈ ℤ
9. b1 = (b|¬y) ∈ bag(Atom)
⊢ 0 = 1 ∈ |r|

2
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. b1 : bag(Atom)
6. ¬0 < (#y in b1)
7. b = ((b|y) + (b|¬y)) ∈ bag(Atom)
8. n < #(b1)
9. #(b) = n ∈ ℤ
⊢ 0 = if bag-eq(AtomDeq;b1;(b|¬y)) then 1 else 0 fi  ∈ |r|

3
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. b1 : bag(Atom)
6. ¬n < #(b1)
7. ¬0 < (#y in b1)
8. b = ((b|y) + (b|¬y)) ∈ bag(Atom)
9. (b1 + bag-rep(n - #(b1);y)) = b ∈ bag(Atom)
⊢ 1 = (if (#(b) =z n) then λb@0.if bag-eq(AtomDeq;b@0;(b|¬y)) then 1 else 0 fi  else λb.0 fi  b1) ∈ |r|

4
1. r : CRng
2. y : Atom
3. n : ℕ
4. b : bag(Atom)
5. b1 : bag(Atom)
6. ¬((b1 + bag-rep(n - #(b1);y)) = b ∈ bag(Atom))
7. ¬n < #(b1)
8. ¬0 < (#y in b1)
9. b = ((b|y) + (b|¬y)) ∈ bag(Atom)
⊢ 0 = (if (#(b) =z n) then λb@0.if bag-eq(AtomDeq;b@0;(b|¬y)) then 1 else 0 fi  else λb.0 fi  b1) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[y:Atom].  \mforall{}[n:\mBbbN{}].  \mforall{}[b:bag(Atom)].
    ([<b>]\_n(y:=1)  =  if  (\#(b)  =\msubz{}  n)  then  <(b|\mneg{}y)>  else  0  fi  )


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  (InstLemma  `bag-restrict-split`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``fps-zero  fps-single  fps-coeff  fps-set-to-one``  0
  THEN  RepeatFor  3  (AutoSplit)
  THEN  Try  (((RWO  "eqtt\_to\_assert  eqff\_to\_assert"  (-1)  THENA  Auto)
                        THEN  RW  assert\_pushdownC  (-1)
                        THEN  Auto')))

---

Home Index