---

{ [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,  uall: [x:A]. B[x],  top: Top,  list: type List,  sqequal: s ~ t
Definitions :  manames-overlap-case: if nms1 and nms2 overlap then x else y fi,  branch: if p:P then A[p] else B fi ,  member: t  T,  all: x:A. B[x],  prop: ,  implies: P  Q,  decidable: Dec(P),  uall: [x:A]. B[x],  or: P  Q,  not: A,  false: False,  uiff: uiff(P;Q),  and: P  Q,  uimplies: b supposing a
Lemmas :  MaName_wf,  decidable_wf,  l_disjoint_wf,  l_disjoint-symmetry,  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: 2011_08_10-AM-07_52_19
Last ObjectModification: 2011_06_18-AM-08_14_31

Home Index