autotests/folding/test.mm.fold

0001 <beginfold id='1'>$(</beginfold id='1'> Modified version of demo0.mm from 1-Jan-04 <endfold id='1'>$)</endfold id='1'>
0002
0003 <beginfold id='1'>$(</beginfold id='1'>
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 <endfold id='1'>$)</endfold id='1'>
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 <beginfold id='2'>${</beginfold id='2'>
0031     <beginfold id='1'>$(</beginfold id='1'> Define the modus ponens inference rule <endfold id='1'>$)</endfold id='1'>
0032     min $e |- P $.
0033     maj $e |- ( P -> Q ) $.
0034     mp  $a |- Q $.
0035 <endfold id='2'>$}</endfold id='2'>
0036
0037 th1 $p |- t = t <beginfold id='3'>$=</beginfold id='3'>
0038     <beginfold id='1'>$(</beginfold id='1'> Here is its proof: <endfold id='1'>$)</endfold id='1'>
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 <endfold id='3'>$.</endfold id='3'>