From 20d9c447551de9c81e1658b85fe3c1728cf92eeb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 12 Mar 2009 09:37:27 +0000 Subject: [PATCH] More details on the proof. --- .../matita/contribs/formal_topology/bin/comb.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 -- 2.39.2