Step
*
1
1
of Lemma
bag-append-is-single
1. T : Type
2. x : T
3. u : T
4. v : T 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