Step
*
1
1
1
1
1
1
of Lemma
oal_dom_merge
1. a : LOSet@i'
2. b : AbDMon@i'
3. ps : |oal(a;b)|@i
4. qs : |oal(a;b)|@i
5. u : |a|@i
6. (↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps). (¬b(x (=b) u)))) ∧ (↑(∀bx(:|a|) ∈ map(λz.(fst(z));qs). (¬b(x (=b) u))))
⊢ ↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps ++ qs)
(¬b(x (=b) u)))
BY
{ % Finally, we can apply this lemma %
((BLemma `oal_merge_dom_pred`) THEN Auto) }
Latex:
Latex:
1. a : LOSet@i'
2. b : AbDMon@i'
3. ps : |oal(a;b)|@i
4. qs : |oal(a;b)|@i
5. u : |a|@i
6. (\muparrow{}(\mforall{}\msubb{}x(:|a|) \mmember{} map(\mlambda{}z.(fst(z));ps)
(\mneg{}\msubb{}(x (=\msubb{}) u))))
\mwedge{} (\muparrow{}(\mforall{}\msubb{}x(:|a|) \mmember{} map(\mlambda{}z.(fst(z));qs)
(\mneg{}\msubb{}(x (=\msubb{}) u))))
\mvdash{} \muparrow{}(\mforall{}\msubb{}x(:|a|) \mmember{} map(\mlambda{}z.(fst(z));ps ++ qs)
(\mneg{}\msubb{}(x (=\msubb{}) u)))
By
Latex:
\% Finally, we can apply this lemma \%
((BLemma `oal\_merge\_dom\_pred`) THEN Auto)
Home
Index