File: test.mm.html

package info (click to toggle)
kf6-syntax-highlighting 6.13.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 47,568 kB
  • sloc: xml: 197,750; cpp: 12,850; python: 3,023; sh: 955; perl: 546; ruby: 488; pascal: 393; javascript: 161; php: 150; jsp: 132; lisp: 131; haskell: 124; ada: 119; ansic: 107; makefile: 96; f90: 94; ml: 85; cobol: 81; yacc: 71; csh: 62; erlang: 54; sql: 51; java: 47; objc: 37; awk: 31; asm: 30; tcl: 29; fortran: 18; cs: 10
file content (49 lines) | stat: -rw-r--r-- 4,698 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
 
<!DOCTYPE html>
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<title>test.mm</title>
<meta name="generator" content="KF5::SyntaxHighlighting - Definition (Metamath) - Theme (Breeze Light)"/>
</head><body style="background-color:#ffffff;color:#1f1c1b"><pre>
<span style="color:#898887">$( Modified version of demo0.mm from 1-Jan-04 $)</span>

<span style="color:#898887">$(</span>
<span style="color:#898887">                      PUBLIC DOMAIN DEDICATION</span>

<span style="color:#898887">This file is placed in the public domain per the Creative Commons Public</span>
<span style="color:#898887">Domain Dedication. http://creativecommons.org/licenses/publicdomain/</span>

<span style="color:#898887">Norman Megill - email: nm at alum.mit.edu</span>
<span style="color:#898887">$)</span>

<span style="font-weight:bold">$c</span><span style="color:#644a9b"> 0 + = -> ( ) term wff |- </span><span style="font-weight:bold">$.</span>

<span style="font-weight:bold">$v</span><span style="color:#0057ae"> t r s P Q </span><span style="font-weight:bold">$.</span>

<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>
<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>
<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>
<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>
<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>

<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>
<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>

<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>
<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>

<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>
<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>
<span style="font-weight:bold">${</span>
    <span style="color:#898887">$( Define the modus ponens inference rule $)</span>
    <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>
    <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>
    <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>
<span style="font-weight:bold">$}</span>

<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>
<span style="color:#ff5500">    </span><span style="color:#898887">$( Here is its proof: $)</span>
<span style="color:#ff5500">    tt tze tpl tt weq tt tt weq tt a2 tt tze tpl</span>
<span style="color:#ff5500">    tt weq tt tze tpl tt weq tt tt weq wim tt a2</span>
<span style="color:#ff5500">    tt tze tpl tt tt a1 mp mp</span>
<span style="font-weight:bold">$.</span>
</pre></body></html>