autotests/reference/test.mm.ref

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