---

Step * 1 of Lemma null-bag-size


1. T : Type
2. x : bag(T)
⊢ bag-null(x) = (#(x) =z 0)
BY
{ AutoBoolCase ⌜(#(x) =z 0)⌝⋅ }

1
1. T : Type
2. x : bag(T)
3. #(x) = 0 ∈ ℤ
⊢ bag-null(x) = tt

2
1. T : Type
2. x : bag(T)
3. #(x) ≠ 0
⊢ bag-null(x) = ff

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  bag(T)
\mvdash{}  bag-null(x)  =  (\#(x)  =\msubz{}  0)


By

---

Latex:
AutoBoolCase  \mkleeneopen{}(\#(x)  =\msubz{}  0)\mkleeneclose{}\mcdot{}

---

Home Index