---

Step * of Lemma bag-append-equal-bag-rep

No Annotations
∀[T:Type]. ∀[x:T]. ∀[n:ℕ]. ∀[a,b:bag(T)].
  uiff((a + b) = bag-rep(n;x) ∈ bag(T);(n = (#(a) + #(b)) ∈ ℤ)
  ∧ (a = bag-rep(#(a);x) ∈ bag(T))
  ∧ (b = bag-rep(#(b);x) ∈ bag(T)))
BY
{ TACTIC:Auto }

1
1. T : Type
2. x : T
3. n : ℕ
4. a : bag(T)
5. b : bag(T)
6. (a + b) = bag-rep(n;x) ∈ bag(T)
⊢ n = (#(a) + #(b)) ∈ ℤ

2
1. T : Type
2. x : T
3. n : ℕ
4. a : bag(T)
5. b : bag(T)
6. (a + b) = bag-rep(n;x) ∈ bag(T)
⊢ a = bag-rep(#(a);x) ∈ bag(T)

3
1. T : Type
2. x : T
3. n : ℕ
4. a : bag(T)
5. b : bag(T)
6. (a + b) = bag-rep(n;x) ∈ bag(T)
⊢ b = bag-rep(#(b);x) ∈ bag(T)

4
1. T : Type
2. x : T
3. n : ℕ
4. a : bag(T)
5. b : bag(T)
6. n = (#(a) + #(b)) ∈ ℤ
7. a = bag-rep(#(a);x) ∈ bag(T)
8. b = bag-rep(#(b);x) ∈ bag(T)
⊢ (a + b) = bag-rep(n;x) ∈ bag(T)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}].  \mforall{}[a,b:bag(T)].
    uiff((a  +  b)  =  bag-rep(n;x);(n  =  (\#(a)  +  \#(b)))  \mwedge{}  (a  =  bag-rep(\#(a);x))  \mwedge{}  (b  =  bag-rep(\#(b);x)))


By

---

Latex:
TACTIC:Auto

---

Home Index