the next generation of the in-browser educational proof assistant
add some rules about eq
+15
-5
+15
-5
index.html
+15
-5
index.html
···
329
329
(P 0)
330
330
[k. (P k) |- (P (S (S k)))]
331
331
--------------------------- E-ind
332
-
(P n) </hol-comp>
332
+
(P n)
333
+
334
+
a.
335
+
---- refl
336
+
(= a a)
337
+
338
+
a. b. f.
339
+
(= a b) (f a)
340
+
-------- eq-ap
341
+
(f b)
342
+
</hol-comp>
333
343
<hol-config id="index.html/myconfig">Gentzen</hol-config>
334
344
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
335
-
a.
336
-
(Nat a)
345
+
a. b. f.
346
+
(= a b)
337
347
-------
338
-
(Nat (S (S a)))
348
+
(= (f a) (f b))
339
349
340
-
a. asm |- ?
350
+
a. b. f. asm |- ?
341
351
</hol-proof>
342
352
<h1>String</h1>
343
353
<h2>Basic</h2>