X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=8566c972630e3435160cb4cc772c425169edb34b;hpb=f757483a6beb4ed12c9959c07567e8891a2b3048;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 8566c9726..4a801a654 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -40,10 +40,14 @@ which generates the toplevel element (see for instance xlink) -->
xmlns:xlink="http://www.w3.org/1999/xlink">
-
+
+
+
+
+
@@ -177,10 +181,54 @@ which generates the toplevel element (see for instance xlink) -->
-
+
__
- :
-
+
+
+
+
+
+
+
+
+
+ _
+
+
+ :
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ :=
+
+
+
+
+
+ _
+ :?
+ _
+
+
+
+
+ ;
+
+
+ |-
+ ?
+ :
+
@@ -188,7 +236,7 @@ which generates the toplevel element (see for instance xlink) -->
- CORRESPONDING PROOF:
+ PROOF:
@@ -356,6 +404,61 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ none
+
+
+ solid
+
+
+
+ ?
+ :
+ _
+
+
+
+
+
+
+
+
+ :
+
+
+ :=
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -371,21 +474,27 @@ which generates the toplevel element (see for instance xlink) -->
-
- :
+
+
+ :
+
+
+
-
- :
-
+
+
+ :
+
+
@@ -403,10 +512,20 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
+
+
+
+
+
+
+
+
+
+
@@ -415,7 +534,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
@@ -431,7 +550,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
:
@@ -605,7 +724,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -614,7 +736,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -630,10 +755,16 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
@@ -729,8 +860,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -743,10 +874,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -757,7 +888,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -779,15 +910,15 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
@@ -979,24 +1110,173 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
- we proved
- _
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+ we proved
+ _
+
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+ we proved
+ _
+
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1004,28 +1284,25 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
-
-
-
- We prove
+ We prove
_
@@ -1034,9 +1311,9 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
-
@@ -1044,12 +1321,13 @@ which generates the toplevel element (see for instance xlink) -->
- _
-
+
+
+
@@ -1065,7 +1343,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1079,7 +1357,9 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+
+ By induction hypothesis, we have:
+
@@ -1099,7 +1379,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
@@ -1129,6 +1411,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -1147,8 +1430,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1252,7 +1533,7 @@ which generates the toplevel element (see for instance xlink) -->
- Then apply it to
+ Then apply it to
_
@@ -1282,7 +1563,7 @@ which generates the toplevel element (see for instance xlink) -->
- In particular, we have
+ In particular, we have
@@ -1317,8 +1598,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1341,7 +1620,7 @@ which generates the toplevel element (see for instance xlink) -->
- We proceed by cases to prove
+ We proceed by cases to prove
_
@@ -1350,7 +1629,7 @@ which generates the toplevel element (see for instance xlink) -->
- Left: suppose
+ Left: suppose
_
(
@@ -1362,8 +1641,8 @@ which generates the toplevel element (see for instance xlink) -->
- _
+ _
@@ -1371,7 +1650,7 @@ which generates the toplevel element (see for instance xlink) -->
- Right: suppose
+ Right: suppose
_
(
@@ -1390,7 +1669,6 @@ which generates the toplevel element (see for instance xlink) -->
-
@@ -1413,11 +1691,11 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
_
- by cases:
+ by cases:
@@ -1467,7 +1745,7 @@ which generates the toplevel element (see for instance xlink) -->
:
_
- such that
+ such that
_
(
@@ -1486,6 +1764,217 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1519,7 +2008,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1537,7 +2026,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1553,7 +2042,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1587,256 +2081,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -1894,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
+
+
+
+
@@ -1920,5 +2173,3 @@ which generates the toplevel element (see for instance xlink) -->
-
-