Warning, file /frameworks/syntax-highlighting/autotests/html/test.mm.html was not indexed or was modified since last indexation (in which case cross-reference links may be missing, inaccurate or erroneous).
0001 <!DOCTYPE html> 0002 <html><head> 0003 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/> 0004 <title>test.mm</title> 0005 <meta name="generator" content="KF5::SyntaxHighlighting - Definition (Metamath) - Theme (Breeze Light)"/> 0006 </head><body style="background-color:#ffffff;color:#1f1c1b"><pre> 0007 <span style="color:#898887;">$( Modified version of demo0.mm from 1-Jan-04 $)</span> 0008 0009 <span style="color:#898887;">$(</span> 0010 <span style="color:#898887;"> PUBLIC DOMAIN DEDICATION</span> 0011 0012 <span style="color:#898887;">This file is placed in the public domain per the Creative Commons Public</span> 0013 <span style="color:#898887;">Domain Dedication. http://creativecommons.org/licenses/publicdomain/</span> 0014 0015 <span style="color:#898887;">Norman Megill - email: nm at alum.mit.edu</span> 0016 <span style="color:#898887;">$)</span> 0017 0018 <span style="font-weight:bold;">$c</span><span style="color:#644a9b;"> 0 + = -> ( ) term wff |- </span><span style="font-weight:bold;">$.</span> 0019 0020 <span style="font-weight:bold;">$v</span><span style="color:#0057ae;"> t r s P Q </span><span style="font-weight:bold;">$.</span> 0021 0022 <span style="color:#ff5500;">tt</span> <span style="font-weight:bold;">$f</span> <span style="color:#644a9b;">term</span><span style="color:#0057ae;"> t </span><span style="font-weight:bold;">$.</span> 0023 <span style="color:#ff5500;">tr</span> <span style="font-weight:bold;">$f</span> <span style="color:#644a9b;">term</span><span style="color:#0057ae;"> r </span><span style="font-weight:bold;">$.</span> 0024 <span style="color:#ff5500;">ts</span> <span style="font-weight:bold;">$f</span> <span style="color:#644a9b;">term</span><span style="color:#0057ae;"> s </span><span style="font-weight:bold;">$.</span> 0025 <span style="color:#ff5500;">wp</span> <span style="font-weight:bold;">$f</span> <span style="color:#644a9b;">wff</span><span style="color:#0057ae;"> P </span><span style="font-weight:bold;">$.</span> 0026 <span style="color:#ff5500;">wq</span> <span style="font-weight:bold;">$f</span> <span style="color:#644a9b;">wff</span><span style="color:#0057ae;"> Q </span><span style="font-weight:bold;">$.</span> 0027 0028 <span style="color:#ff5500;">tze</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">term</span><span style="color:#0057ae;"> 0 </span><span style="font-weight:bold;">$.</span> 0029 <span style="color:#ff5500;">tpl</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">term</span><span style="color:#0057ae;"> ( t + r ) </span><span style="font-weight:bold;">$.</span> 0030 0031 <span style="color:#ff5500;">weq</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">wff</span><span style="color:#0057ae;"> t = r </span><span style="font-weight:bold;">$.</span> 0032 <span style="color:#ff5500;">wim</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">wff</span><span style="color:#0057ae;"> ( P -> Q ) </span><span style="font-weight:bold;">$.</span> 0033 0034 <span style="color:#ff5500;">a1</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> ( t = r -> ( t = s -> r = s ) ) </span><span style="font-weight:bold;">$.</span> 0035 <span style="color:#ff5500;">a2</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> ( t + 0 ) = t </span><span style="font-weight:bold;">$.</span> 0036 <span style="font-weight:bold;">${</span> 0037 <span style="color:#898887;">$( Define the modus ponens inference rule $)</span> 0038 <span style="color:#ff5500;">min</span> <span style="font-weight:bold;">$e</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> P </span><span style="font-weight:bold;">$.</span> 0039 <span style="color:#ff5500;">maj</span> <span style="font-weight:bold;">$e</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> ( P -> Q ) </span><span style="font-weight:bold;">$.</span> 0040 <span style="color:#ff5500;">mp</span> <span style="font-weight:bold;">$a</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> Q </span><span style="font-weight:bold;">$.</span> 0041 <span style="font-weight:bold;">$}</span> 0042 0043 <span style="color:#ff5500;">th1</span> <span style="font-weight:bold;">$p</span> <span style="color:#644a9b;">|-</span><span style="color:#0057ae;"> t = t </span><span style="font-weight:bold;">$=</span> 0044 <span style="color:#ff5500;"> </span><span style="color:#898887;">$( Here is its proof: $)</span> 0045 <span style="color:#ff5500;"> tt tze tpl tt weq tt tt weq tt a2 tt tze tpl</span> 0046 <span style="color:#ff5500;"> tt weq tt tze tpl tt weq tt tt weq wim tt a2</span> 0047 <span style="color:#ff5500;"> tt tze tpl tt tt a1 mp mp</span> 0048 <span style="font-weight:bold;">$.</span> 0049 </pre></body></html>