X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=d0c8555b39ac48df5c4a91c1469350ffcff0dfdb;hb=5efc24038e24e64e39ec33d4c8f09e1fc6948366;hp=5a9a391d3466dd130f83df6d76ae72e26e304e34;hpb=b205c1fb5ec671d31e051a9a2f0e534b4e393452;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 5a9a391d3..d0c8555b3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -44,6 +44,8 @@ which generates the toplevel element (see for instance xlink) -->
+
+
@@ -62,11 +64,19 @@ which generates the toplevel element (see for instance xlink) -->
+
+
-
-
+
+
+
+
+
+
+
+
+
+
@@ -363,21 +373,27 @@ which generates the toplevel element (see for instance xlink) -->
-
- :
+
+
+ :
+
+
+
-
- :
-
+
+
+ :
+
+
@@ -395,10 +411,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
@@ -406,7 +423,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
@@ -422,7 +439,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
:
@@ -431,6 +448,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -476,6 +494,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -508,6 +527,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -584,6 +604,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -626,6 +647,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -664,15 +686,19 @@ which generates the toplevel element (see for instance xlink) -->
+
Prop
+
Set
+
Type
+
@@ -711,8 +737,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -725,10 +751,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -739,7 +765,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -761,21 +787,22 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
+
@@ -865,6 +892,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -957,7 +985,33 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
@@ -969,14 +1023,24 @@ which generates the toplevel element (see for instance xlink) -->
- we proved
+ we proved
_
+
+
+ _
+
+
+ (hide details)
+
+
+
+
@@ -995,6 +1059,140 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+ We prove
+ _
+
+
+
+
+
+
+
+ by induction on
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Case
+ _
+
+
+
+
+
+
+
+ _
+
+
+
+
+
+ By induction hypothesis, we have:
+
+
+
+
+
+
+ _
+
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+
+ _
+
+ :
+
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Contradiction.
+
+
+
+
+
+
@@ -1016,12 +1214,14 @@ which generates the toplevel element (see for instance xlink) -->
+
(
)
+
@@ -1082,6 +1282,7 @@ which generates the toplevel element (see for instance xlink) -->
-->
+
@@ -1094,7 +1295,7 @@ which generates the toplevel element (see for instance xlink) -->
- Then apply it to
+ Then apply it to
_
@@ -1102,34 +1303,65 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
- By induction
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
- base case:
-
+ In particular, we have
- inductive case:
+ (
+ )
+ _
+
+
+
+
+
+
+
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
-
-
+
+
@@ -1150,41 +1382,56 @@ which generates the toplevel element (see for instance xlink) -->
- In particular, we have
+ We proceed by cases to prove
+ _
+
- (
-
- )
+ Left: suppose
_
-
-
+ (
+
+ )
+ _
+
+
- (
-
- )
_
-
-
+
+
-
+ Right: suppose
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
@@ -1206,18 +1453,18 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
_
- by cases:
+ by cases:
- *
+ Left
@@ -1225,13 +1472,14 @@ which generates the toplevel element (see for instance xlink) -->
- *
+ Right
+
@@ -1259,7 +1507,7 @@ which generates the toplevel element (see for instance xlink) -->
:
_
- such that
+ such that
_
(
@@ -1278,8 +1526,134 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
+
- ERROR
+ ERROR
@@ -1310,7 +1684,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1328,7 +1702,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1344,7 +1718,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1391,7 +1770,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1409,7 +1788,12 @@ which generates the toplevel element (see for instance xlink) -->
__
- =
+
+
+
+
+
+ =
@@ -1438,43 +1822,43 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -1484,7 +1868,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1502,9 +1886,12 @@ which generates the toplevel element (see for instance xlink) -->
__
-
-
-
+
+
+
+
+
+
@@ -1528,9 +1915,12 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
+
+
+
+
+
+ ∅
@@ -1544,7 +1934,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
@@ -1561,7 +1956,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1572,7 +1972,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
,
@@ -1596,7 +2001,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1623,11 +2033,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
@@ -1710,6 +2115,3 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-