autotests/input/test.mm

0001 $( Modified version of demo0.mm from 1-Jan-04 $)
0002
0003 $(
0004                       PUBLIC DOMAIN DEDICATION
0005
0006 This file is placed in the public domain per the Creative Commons Public
0007 Domain Dedication. http://creativecommons.org/licenses/publicdomain/
0008
0009 Norman Megill - email: nm at alum.mit.edu
0010 $)
0011
0012 $c 0 + = -> ( ) term wff |- $.
0013
0014 $v t r s P Q $.
0015
0016 tt $f term t $.
0017 tr $f term r $.
0018 ts $f term s $.
0019 wp $f wff P $.
0020 wq $f wff Q $.
0021
0022 tze $a term 0 $.
0023 tpl $a term ( t + r ) $.
0024
0025 weq $a wff t = r $.
0026 wim $a wff ( P -> Q ) $.
0027
0028 a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
0029 a2 $a |- ( t + 0 ) = t $.
0030 ${
0031     $( Define the modus ponens inference rule $)
0032     min $e |- P $.
0033     maj $e |- ( P -> Q ) $.
0034     mp  $a |- Q $.
0035 $}
0036
0037 th1 $p |- t = t $=
0038     $( Here is its proof: $)
0039     tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
0040     tt weq tt tze tpl tt weq tt tt weq wim tt a2
0041     tt tze tpl tt tt a1 mp mp
0042 $.