diff --git a/autotests/folding/test.mm.fold b/autotests/folding/test.mm.fold
new file mode 100644
--- /dev/null
+++ b/autotests/folding/test.mm.fold
@@ -0,0 +1,42 @@
+
+$( Modified version of demo0.mm from 1-Jan-04 $) + +$( + PUBLIC DOMAIN DEDICATION + +This file is placed in the public domain per the Creative Commons Public +Domain Dedication. http://creativecommons.org/licenses/publicdomain/ + +Norman Megill - email: nm at alum.mit.edu +$) + +$c 0 + = -> ( ) term wff |- $. + +$v t r s P Q $. + +tt $f term t $. +tr $f term r $. +ts $f term s $. +wp $f wff P $. +wq $f wff Q $. + +tze $a term 0 $. +tpl $a term ( t + r ) $. + +weq $a wff t = r $. +wim $a wff ( P -> Q ) $. + +a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. +a2 $a |- ( t + 0 ) = t $. +${ + $( Define the modus ponens inference rule $) + min $e |- P $. + maj $e |- ( P -> Q ) $. + mp $a |- Q $. +$} + +th1 $p |- t = t $= + $( Here is its proof: $) + tt tze tpl tt weq tt tt weq tt a2 tt tze tpl + tt weq tt tze tpl tt weq tt tt weq wim tt a2 + tt tze tpl tt tt a1 mp mp +$. +diff --git a/autotests/input/test.mm b/autotests/input/test.mm new file mode 100644 --- /dev/null +++ b/autotests/input/test.mm @@ -0,0 +1,42 @@ +$( Modified version of demo0.mm from 1-Jan-04 $) + +$( + PUBLIC DOMAIN DEDICATION + +This file is placed in the public domain per the Creative Commons Public +Domain Dedication. http://creativecommons.org/licenses/publicdomain/ + +Norman Megill - email: nm at alum.mit.edu +$) + +$c 0 + = -> ( ) term wff |- $. + +$v t r s P Q $. + +tt $f term t $. +tr $f term r $. +ts $f term s $. +wp $f wff P $. +wq $f wff Q $. + +tze $a term 0 $. +tpl $a term ( t + r ) $. + +weq $a wff t = r $. +wim $a wff ( P -> Q ) $. + +a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. +a2 $a |- ( t + 0 ) = t $. +${ + $( Define the modus ponens inference rule $) + min $e |- P $. + maj $e |- ( P -> Q ) $. + mp $a |- Q $. +$} + +th1 $p |- t = t $= + $( Here is its proof: $) + tt tze tpl tt weq tt tt weq tt a2 tt tze tpl + tt weq tt tze tpl tt weq tt tt weq wim tt a2 + tt tze tpl tt tt a1 mp mp +$. diff --git a/autotests/input/test.mm.syntax b/autotests/input/test.mm.syntax new file mode 100644 --- /dev/null +++ b/autotests/input/test.mm.syntax @@ -0,0 +1 @@ +Metamath diff --git a/autotests/reference/test.mm.ref b/autotests/reference/test.mm.ref new file mode 100644 --- /dev/null +++ b/autotests/reference/test.mm.ref @@ -0,0 +1,42 @@ +