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