Warning, /frameworks/syntax-highlighting/autotests/folding/test.mm.fold is written in an unsupported language. File is not indexed.
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'>