Step
*
1
of Lemma
omral_dom_scale
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. x : |(g↓oset)|
7. ↑(x
∈b dom(<k,v>* ps))
⊢ ↑(x
∈b fs-map(λk'.(k' * k), dom(ps)))
BY
{ ((Decide ↑(x
∈b fs-map(λk'.(k' * k), dom(ps))) THENA Auto THEN Try Trivial THENM Negate 7⋅) THENA Auto) }
1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. x : |(g↓oset)|
7. ¬↑(x
∈b fs-map(λk'.(k' * k), dom(ps)))
⊢ ¬↑(x
∈b dom(<k,v>* ps))
Latex:
Latex:
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. x : |(g\mdownarrow{}oset)|
7. \muparrow{}(x
\mmember{}\msubb{} dom(<k,v>* ps))
\mvdash{} \muparrow{}(x
\mmember{}\msubb{} fs-map(\mlambda{}k'.(k' * k), dom(ps)))
By
Latex:
((Decide \muparrow{}(x
\mmember{}\msubb{} fs-map(\mlambda{}k'.(k' * k), dom(ps))) THENA Auto THEN Try Trivial THENM Negate 7\mcdot{}) THENA Auto)
Home
Index