X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=fad3dce6b333edad5e4b32d06e5baa38c34cca9d;hb=000ee25879c192864cfaa0ebc27cc91a896378df;hp=a4dfc5f01e7210c6ecc3aca3246cbe4b322c23fb;hpb=ce56bfc29034be5add28ef28007f2598d9030ad2;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index a4dfc5f01..fad3dce6b 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,21 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -414,7 +534,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
@@ -430,7 +550,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
:
@@ -439,6 +559,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -484,6 +605,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -516,6 +638,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -592,6 +715,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -600,7 +724,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -609,7 +736,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -625,15 +755,22 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
+
@@ -672,15 +809,19 @@ which generates the toplevel element (see for instance xlink) -->
+
Prop
+
Set
+
Type
+
@@ -719,8 +860,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -733,10 +874,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -747,7 +888,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -769,21 +910,22 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
+
@@ -873,6 +1015,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -962,10 +1105,271 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+ {
+
+
+ :=
+
+
+ }
+
+
+
+
+
+
+
+
+
+
+
+ @
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ @
+
+
+
+
+
+
+
+
+
+
+
+
+
+ if
+
+
+
+
+
+
+
+ then
+
+
+
+
+
+
+
+ else
+
+
+
+
+
+
+
+
+ if
+
+ then
+
+ else
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+ we proved
+ _
+
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+ we proved
+ _
+
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -977,32 +1381,146 @@ which generates the toplevel element (see for instance xlink) -->
- we proved
- _
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+ We prove
+ _
+
+
+
+
+
+
+
+ by induction on
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Case
+ _
+
+
+
+
+
+
+
+ _
+
+
+
+
+
+ By induction hypothesis, we have:
+
+
+
+
+
+
+ _
+
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+
+ _
+
+ :
+
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Contradiction.
+
+
+
+
+
@@ -1024,12 +1542,14 @@ which generates the toplevel element (see for instance xlink) -->
+
(
)
+
@@ -1048,27 +1568,116 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
- Rewrite
- _
-
- _
- with
- _
-
- _
- by
- _
-
-
-
-
-
-
-
-->
+
@@ -1102,7 +1712,7 @@ which generates the toplevel element (see for instance xlink) -->
- Then apply it to
+ Then apply it to
_
@@ -1110,34 +1720,65 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
- By induction
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
- base case:
-
+ In particular, we have
- inductive case:
+ (
+ )
+ _
+
+
+
+
+
+
+
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
-
-
+
+
@@ -1158,41 +1799,56 @@ which generates the toplevel element (see for instance xlink) -->
- In particular, we have
+ We proceed by cases to prove
+ _
+
- (
-
- )
+ Left: suppose
_
-
-
+ (
+
+ )
+ _
+
+
- (
-
- )
_
-
-
+
+
-
+ Right: suppose
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
@@ -1214,18 +1870,18 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
_
- by cases:
+ by cases:
- *
+ Left
@@ -1233,13 +1889,14 @@ which generates the toplevel element (see for instance xlink) -->
- *
+ Right
+
@@ -1267,7 +1924,7 @@ which generates the toplevel element (see for instance xlink) -->
:
_
- such that
+ such that
_
(
@@ -1286,8 +1943,220 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
+
- ERROR
+ ERROR("")
@@ -1318,7 +2187,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1336,7 +2205,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1352,7 +2221,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1386,261 +2260,29 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
-
+
+
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -1668,14 +2310,24 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
+
+
+
+ 3
+
+
+
+
+
+
-
-
+
+
-
+
@@ -1683,7 +2335,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1693,7 +2345,16 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
+
+
+
+
@@ -1719,5 +2380,3 @@ which generates the toplevel element (see for instance xlink) -->
-
-