Step
*
of Lemma
bag-val_wf
∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T]. (Comm(T;+)
⇒ Assoc(T;+)
⇒ Ident(T;+;zero)
⇒ (bag-val(zero;+) ∈ bag(T) ⟶ T))
BY
{ (Auto THEN Unfold `bag-val` 0 THEN MemCD THEN Try (Complete (Auto))) }
1
.....subterm..... T:t
1:n
1. T : Type
2. + : T ⟶ T ⟶ T
3. zero : T
4. Comm(T;+)
5. Assoc(T;+)
6. Ident(T;+;zero)
7. b : bag(T)
⊢ accumulate (with value v and list item x):
v + x
over list:
b
with starting value:
zero) ∈ T
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[+:T {}\mrightarrow{} T {}\mrightarrow{} T]. \mforall{}[zero:T].
(Comm(T;+) {}\mRightarrow{} Assoc(T;+) {}\mRightarrow{} Ident(T;+;zero) {}\mRightarrow{} (bag-val(zero;+) \mmember{} bag(T) {}\mrightarrow{} T))
By
Latex:
(Auto THEN Unfold `bag-val` 0 THEN MemCD THEN Try (Complete (Auto)))
Home
Index