From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 12 Mar 2009 09:37:27 +0000 (+0000)
Subject: More details on the proof.
X-Git-Tag: make_still_working~4152
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20d9c447551de9c81e1658b85fe3c1728cf92eeb;p=helm.git

More details on the proof.
---

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 5734c618d..f998b88a9 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -16,6 +16,16 @@ cMw = CMw
 -MMw = -w
 -MCw = MMCw
 iw = w
+
+
+  s <= s'            s <= s'         s <= s'           s <= s'
+===========        ===========     ============      ==========
+ ws <= Cws'         Cs <= Cs'       CMs' <= Ms       Ms' <= MCs
+
+  s <= s'          s <= s'
+===========     ============
+ s <= MMs'        Ms' <= Ms
+
 *)
 
 type t = M | I | C