Nuprl Lemma : manames-overlap-case-symmetry
∀[x,y:Top]. ∀[nms1,nms2:MaName List].
(if nms1 and nms2 overlap then x else y fi ~ if nms2 and nms1 overlap then x else y fi)
Proof
Definitions occuring in Statement :
manames-overlap-case: if nms1 and nms2 overlap then x else y fi,
MaName: MaName,
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
all_wf,
list_wf,
MaName_wf,
decidable_wf,
l_disjoint_wf,
l_disjoint-symmetry,
equal_wf,
top_wf
\mforall{}[x,y:Top]. \mforall{}[nms1,nms2:MaName List].
(if nms1 and nms2 overlap then x else y fi \msim{} if nms2 and nms1 overlap then x else y fi)
Date html generated:
2015_07_17-AM-09_15_04
Last ObjectModification:
2015_01_28-AM-07_54_27
Home
Index