Step * 1 1 of Lemma bag-append-is-single


1. Type
2. T
3. T
4. List
5. ((v []) {x} ∈ bag(T))  (↓((v {x} ∈ bag(T)) ∧ ([] {} ∈ bag(T))) ∨ (([] {x} ∈ bag(T)) ∧ (v {} ∈ bag(T))))
6. ([u v] []) {x} ∈ bag(T)
⊢ [u v] {x} ∈ bag(T)
BY
(NthHypEqTrans (-1) THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  x  :  T
3.  u  :  T
4.  v  :  T  List
5.  ((v  +  [])  =  \{x\})  {}\mRightarrow{}  (\mdownarrow{}((v  =  \{x\})  \mwedge{}  ([]  =  \{\}))  \mvee{}  (([]  =  \{x\})  \mwedge{}  (v  =  \{\})))
6.  ([u  /  v]  +  [])  =  \{x\}
\mvdash{}  [u  /  v]  =  \{x\}


By


Latex:
(NthHypEqTrans  (-1)  THEN  Auto)




Home Index