forked from yetanotherflower/mm0
-
Notifications
You must be signed in to change notification settings - Fork 1
/
peano.mm1
6784 lines (5843 loc) · 318 KB
/
peano.mm1
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
delimiter $ ( [ { ~ $
$ } ] ) , $;
--| Well formed formulas, or propositions - true or false.
strict provable sort wff;
--| Implication: if p, then q.
term im (p q: wff): wff; infixr im: $->$ prec 25;
--| Negation: p is false.
term not (p: wff): wff; prefix not: $~$ prec 41;
--| Axiom 1 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_1 (a b: wff): $ a -> b -> a $;
--| Axiom 2 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $;
--| Axiom 3 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $;
--| Modus ponens: from `a -> b` and `a`, infer `b`.
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;
-- global definitions
do {
(def (id x) x)
(def (ignore . _))
(def dbg @ match-fn* [(x) (print x) x]
[(x y) (display @ string-append (->string x) ": " (->string y)) y])
(def (foldl l z s) (if (null? l) z (foldl (tl l) (s z (hd l)) s)))
(def (foldr l z s) (if (null? l) z (s (hd l) (foldr (tl l) z s))))
(def (range a b) (if {a = b} () (cons a (range {a + 1} b))))
(def (for a b f) (if {a = b} #undef (begin (f a) (for {a + 1} b f))))
(def last (match-fn [(a) a] [(_ . l) (last l)]))
(def split-last @ match-fn
[(and (_) l) l]
[(a . l) @ match (split-last l) @ (r . l2) '(,r ,a . ,l2)]
[() ()])
(def (append . ls) @ foldr ls () @ fn (l l2) @ foldr l l2 cons)
(def (rev l) @ foldl l () (fn (l a) (cons a l)))
(def (len l) @ foldl l 0 (fn (n _) {n + 1}))
(def (filter l p) @ foldl l () @ fn (l2 x) @ if (p x) (cons x l2) l2)
(def (repeat a n) (if {n = 0} () (cons a (repeat a {n - 1}))))
(def (iterate n f a) (if {n = 0} a (f (iterate {n - 1} f a))))
(def (find l) @ match l
[((k v) . l) (def f (find l)) @ fn (a) @ if {k == a} v (f a)]
[() @ fn (a)])
(def (verb e) (copy-span e (list ':verb e)))
(def (exact e) (refine (verb e)))
(def (result) (hd (get-goals)))
(def (target) (goal-type (result)))
(def (inspect-result f) (def g (result)) (refine (f)) (display @ pp g))
(def (later) @ match (get-goals)
[(g . gs) (apply set-goals @ append gs @ list g)])
(def mvar-sort @ match-fn @ (mvar s _) s)
(def (report a) (def g (result)) (refine a) (print g))
(def (atom-map . xs) (get! @ apply atom-map! xs))
(def (lookup-fn xs) (def m (apply atom-map xs)) (fn k (apply lookup m k)))
(def (atom-app . xs) (string->atom (apply string-append (map ->string xs))))
(def transpose @ match-fn*
[(xs) (apply map list xs)]
[(n xs) (if (null? xs) (repeat () n) (apply map list xs))])
(def (join xs) (apply append xs))
(def (rmap . args) (apply map (split-last args)))
(def (scan . args) (apply rmap args) #undef)
(def (undef? x) (not (def? x)))
(def (error-at sp msg) (report-at 'error sp msg))
(def (info-at sp msg) (report-at 'info sp msg))
(def goal! @ match-fn*
[(ty) (ref! (goal ty))]
[(pos ty) (ref! (copy-span pos (goal ty)))])
(def (swap) @ match (get-goals) [(x . y) (apply set-goals @ append y @ list x)])
(def suffices @ match-fn*
[(h) (have h _) (swap)]
[xs (apply have xs) (swap)])
(def (get-proof x) @ match (get-decl x)
[('theorem _ _ _ _ _ pf) (hd @ tl @ pf)]
[_ (error "not a theorem")])
(def (pp-proof x) (display @ pp @ get-proof x))
--| This utility will take a verbatim proof and "unelaborate" it into a refine script
--| using ! on every step. This is useful to get `refine` to re-typecheck a term when
--| testing tactics which produce verbatim proofs (which bypass proof checking, at least ATM).
(def unelab @ letrec (
[(args bs xs)
@ if (null? bs) (map rec xs)
@ cons (hd xs) @ args (tl bs) (tl xs)]
[rec @ match-fn
[(f . xs)
(cons '! f @ args (nth 2 @ get-decl f) xs)]
[e e]])
rec)
--| `(named pf)` wraps a proof script `pf`, runs it, then gathers all
--| unassigned metavariables and assigns them to dummies.
--| `(named x1 ... xn pf)` is the same but names the first `n` variables `x1,...,xn`.
--| This is commonly used for proofs where we don't care to name the
--| dummy variables.
(def named
(def (assign-mvar m x) @ match x ['_] [_ (set! m (dummy! x (mvar-sort m)))])
@ match-fn*
[((? atom? d) es) (refine es) (scan (get-mvars) (list d) assign-mvar)]
[(ds es) (refine es) (scan (get-mvars) ds assign-mvar)]
[(es) (refine es)
(def n (ref! 1))
(scan (get-mvars) @ fn (v)
(assign-mvar v (atom-app "x" n)) (set! n {n + 1}))
(if {n = 1} (display "unnecessary (named)"))])
--| `(name-all x1 ... xn)` instantiates all metavariables in the current
--| proof state. It is the same as `named` but it can be used in the middle of a
--| proof instead of as a wrapper around a complete proof.
(def (name-all . ds)
(def (assign-mvar m x) @ match x ['_] [_ (set! m (dummy! x (mvar-sort m)))])
(scan (get-mvars) ds assign-mvar))
(def ((tac-thm stmt f))
@ match (get-goals) @ (g)
(def res (f))
(if (def? res) (refine res))
(match (get-goals) [()] [_ (stat) (error "not all goals are solved")])
'(() ,g))
(def (add-tac-thm! x bis hyps ret vis f)
(add-thm! x bis hyps ret vis (tac-thm ret f)))
(def eq-for @ lookup-fn '([wff iff] [nat eq] [set eqs]))
(def eq-sort @ lookup-fn '([iff wff] [eq nat] [eqs set]))
(def nf-for @ lookup-fn '([wff nf] [nat nfn] [set nfs]))
(def eqid-for @ lookup-fn '([wff biid] [nat eqid] [set eqsid]))
(def eqidd-for @ lookup-fn '([wff biidd] [nat eqidd] [set eqsidd]))
(def eqd-map (atom-map!)) (set-merge-strategy eqd-map merge-map)
(def (eqd-for . e) (apply lookup eqd-map e))
(def (register-eqd df) (fn (tgt) (insert! eqd-map df tgt)))
(def (get-tgt-args args df . s) @ match args
[() (apply atom-app df s)]
[((? atom? t)) (apply atom-app t s)]
[('quote (? atom? t)) t])
(def (maybe-atom-map hs)
@ if (apply and @ map (fn (x) (atom? (hd x))) hs)
(let ([m (get! @ apply atom-map! hs)])
@ fn (x) (lookup m x))
(find hs))
(def (eqtac-ctx ltr hyps)
@ foldr hyps () @ fn (h ls)
@ match (match (infer-type h) [('im _ R) R] [R R])
[('eq L R) '([,(if ltr L R) ,h] . ,ls)]
[_ ls])
(def (eqtac-core ltr ctx t)
@ match t @ (eq L R)
@ letrec (
[(f A) @ match (ctx A)
[#undef @ match A
[((? atom? t) . es)
@ if (null? es) #undef @ begin
@ match (eqd-for t) [#undef] @ eqd
@ match (get-decl eqd) @ (_ _ bis hs ('im _ (eq (t . args) _)) ...)
(def subterms @ apply atom-map! @ map list args es)
(def isrefl (ref! #t))
(def subproofs @ rmap hs @ match-fn @ (h ('im _ (eq arg _)))
@ if (atom? arg)
(or_refl isrefl @ lookup subterms arg)
(eqidd-for (infer-sort A)))
@ if isrefl #undef (cons eqd subproofs)]
[e #undef]]
[res res]]
[(or_refl isrefl A) @ match (f A)
[#undef (eqidd-for (infer-sort A))]
[e (set! isrefl #f) e]])
(or_refl (ref!) (if ltr L R)))
(def ((eqtac-with ltr . hyps) refine t)
@ refine t @ match t
[('im G (and rhs (eq L R)))
@ letrec ([add-locals @ match-fn*
[(('an G D) f)
(add-locals G @ fn (a p) (f a '(anwl ,G ,D ,a ,p)))
(add-locals D @ fn (a p) (f a '(anwr ,G ,D ,a ,p)))]
[((and a (h . _)) f) @ if (def? (eq-sort h)) (f a '(id ,a))]
[_]])
(def ctx (ref! (eqtac-ctx #t hyps)))
(add-locals G @ match-fn* @ ((eq L R) p)
(def v (if ltr L R))
(def v @ match v [(mvar s _) (def d (dummy! s)) (set! v d) d] [_ v])
(set! ctx '([,v ,(verb p)] . ,(get! ctx))))
(eqtac-core ltr (maybe-atom-map ctx) rhs)]
[(eq L R) '(trud ,(eqtac-core ltr (maybe-atom-map @ eqtac-ctx #t hyps) t))])
--| A refine script that will prove formulas of the form `x = a -> (p <-> ?q)`
--| by substituting all instances of `x` with `a` in `p`. This works whether `?q`
--| is a metavariable or the substitution.
(def eqtac (eqtac-with #t))
--| Like `eqtac` but works in reverse:
--| it will prove formulas of the form `x = a -> (?p <-> q)`
--| by substituting all instances of `a` with `x` in `q`. If `x` is a metavariable, it
--| also assigns it to a new dummy variable.
(def ((eqtac-gen a) refine t) @ refine t
@ match t @ ('im (eq x _) _)
(def y (match x [(mvar s _) (dummy! s)] [_ x]))
'{,(eqtac-with #f) : (im (eq ,y ,a) _)})
--| This metaprogram proves a statement of the form
--| $ G -> a1 = a2 $ > $ G -> b1 = b2 $ > $ G -> foo a1 b1 = foo a2 b2 $
--| for any definition foo.
(def (add-eqd-thm df . args)
(def tgt (get-tgt-args args df "eqd"))
@ match (get-decl df)
[#undef (error (string-append "declaration '" (->string df) "' not found"))]
[(_ _ () ...)]
[(_ _ bis (ret _) . rest)
(def G @ if (apply or (map (match-fn [('G ...) #t] [_ #f]) bis)) '_G '_G)
@ if (def? (get-decl tgt)) (insert! eqd-map df tgt) @ begin
(def ctx (atom-map!))
@ match (map join @ transpose 4 @ rmap bis @ match-fn
[(and (x s) e) (insert! ctx x (list s)) '((,e) () (,x) (,x))]
[(v s vs) @ let ([v1 (atom-app '_ v 1)] [v2 (atom-app '_ v 2)] [hv (atom-app '_ v 'h)])
(insert! ctx v (list v1 v2 s hv))
'(() ((,v ,s ,v1 ,v2 ,hv))
(,v1) (,v2))]) @ (xs vs es1 es2)
(def xs1 (map hd xs))
(def bis '((,G wff ()) . ,(append xs @ join @ rmap vs
@ match-fn [(v s v1 v2 hv) '((,v1 ,s ,xs1) (,v2 ,s ,xs1))])))
(def hs @ rmap vs @ match-fn [(v s v1 v2 hv) '(,hv (im ,G (,(eq-for s) ,v1 ,v2)))])
(def rete '(im ,G (,(eq-for ret) (,df . ,es1) (,df . ,es2))))
(match rest
[() (add-thm! tgt bis hs rete)]
[(_ ds v) @ add-thm! tgt bis hs rete () @ fn () @ list ds
(def ds (rmap ds @ match-fn @ (x s) (insert! ctx x (list s)) x))
@ letrec (
[preproof (match-fn
[(? atom? v) (lookup ctx v)]
[((? atom? t) . es)
@ match (get-decl t) @ (_ _ bis (ret _) ...)
@ if (null? es) (list ret) @ begin
(def isrefl (ref! #t))
@ match (transpose 5 @ rmap bis es @ match-fn*
[((_ _) x) '((,x) () () ,x ,x)]
[((_ _ _) e)
@ match (preproof e)
[(s) '(() (,e ,e) ((,(eqidd-for s) ,G ,e)) ,e ,e)]
[(e1 e2 s p) (set! isrefl #f)
'(() (,e1 ,e2) (,p) ,e1 ,e2)]]) @ (xs ts ps es1 es2)
@ if isrefl (list ret) @ begin
@ match (eqd-for t)
[#undef (error @ string-append "equality theorem not found for " (->string t))]
[eqd '((,t . ,es1) (,t . ,es2) ,ret
(,eqd ,G . ,(append (join xs) (join ts) (join ps))))]])]
[(mk-proof e) (match (preproof e)
[(s) '(,e ,e (,(eqidd-for s) ,G ,e))]
[(e1 e2 s p) (list e1 e2 p)])])
@ match (mk-proof v) @ (t1 t2 p)
'(:conv ,rete (im ,G (,(eq-for ret)
(:unfold ,df ,es1 ,ds ,t1)
(:unfold ,df ,es2 ,ds ,t2))) ,p)])
(insert! eqd-map df tgt)])
(def (ded-to-thm t)
@ match (get-decl t) @ (_ _ ((G 'wff ()) . bis) hs ('im _ ret) ...)
@ if (apply and @ rmap bis @ match-fn [(_ _ ()) #t] [_ #f]) @ begin
(def rete @ foldr hs ret @ match-fn* [((_ ('im _ h)) r) '(im ,h ,r)])
@ list bis rete @ fn () @ list ()
@ letrec (
[(exps l r) @ match r
[('im e1 e2) (list 'exp l e1 e2 (exps (list 'an l e1) e2))]
[_ (cons t l @ append (map hd bis) @
map (match-fn [(_ h) h]) @ rev @ conjuncts l)]]
[conjuncts @ match-fn
[('an e1 e2)
@ match (conjuncts e1)
[(_) '((,e2 (anr ,e1 ,e2)) (,e1 (anl ,e1 ,e2)))]
[hs (cons '(,e2 (anr ,e1 ,e2)) @
rmap hs @ match-fn [(e h) '(,e (anwl ,e1 ,e2 ,e ,h))])]]
[e '((,e (id ,e)))]])
@ match rete [('im l r) (exps l r)])
--| Using the `*eqd` proof in `add-eqd-thm`,
--| this metaprogram proves the corresponding `*eq` theorem of the form
--| `a1 = a2 -> b1 = b2 -> foo a1 b1 = foo a2 b2`
--| for any definition `foo`.
(def (add-eq-thm t . args)
(def tgt (get-tgt-args args t "eq"))
@ if (undef? (get-decl tgt)) @ begin
@ match (eqd-for t) [#undef] @ eqd
@ match (ded-to-thm eqd) [#undef] @ (bis ret val)
(add-thm! tgt bis () ret () val))
(def (make-eqNd-thms df)
@ match (get-decl df) @ (_ _ bis (ret _) . rest)
(def G '_G) (def h0 '_h)
@ letrec (
[mk-bis @ match-fn
[() '(() () () () ())]
[((and (x _) e) . bis)
@ match (mk-bis bis) @ (pes vs es pp data)
'((,x . ,pes) ,vs ,es ,pp
,(rmap data @ match-fn [(b t1 t2 h es ps)
'(,b (,x . ,t1) (,x . ,t2) ,h ,es ,ps)]))]
[((v s _) . bis)
@ match (mk-bis bis) @ (pes vs es pp data)
@ let ([v1 (atom-app '_ v 1)] [v2 (atom-app '_ v 2)])
'((,v . ,pes)
((,v ,s) . ,vs)
(,v ,v . ,es)
((,(eqidd-for s) ,G ,v) . ,pp)
((((,v1 ,s) (,v2 ,s) . ,vs)
(,v1 . ,pes)
(,v2 . ,pes)
(im ,G (,(eq-for s) ,v1 ,v2))
(,v1 ,v2 . ,es)
(,h0 . ,pp)) .
,(rmap data @ match-fn @ (b t1 t2 h es ps)
'(((,v ,s) . ,b) (,v . ,t1) (,v . ,t2) ,h (,v ,v . ,es) ((,(eqidd-for s) ,G ,v) . ,ps)))))]])
(def xs @ join @ rmap bis @ match-fn [(and (_ _) e) (list e)] [_ ()])
@ rmap (match (mk-bis bis) [(_ _ _ _ data) data]) @ match-fn @ (vs t1 t2 h es ps)
(def xs1 (map hd xs))
(def vs+ (rmap vs @ match-fn @ (v s) '(,v ,s ,xs1)))
@ list
'((,G wff ()) . ,(append xs vs+))
'((,h0 ,h))
'(im ,G (,(eq-for ret) (,df . ,t1) (,df . ,t2)))
(match (eqd-for df)
[#undef (error @ string-append "equality theorem not found for " (->string df))]
[eqd '(,eqd ,G . ,(append xs1 es ps))]))
--| This program adds `*eqNd` and `*eqN` theorems corresponding to the definition
--| `foo`, of the form
--| * `fooeq1: $ a1 = a2 -> foo a1 b = foo a2 b $`
--| * `fooeq1: $ a1 = a2 -> foo a1 b = foo a2 b $`
--| * `fooeq2: $ b1 = b2 -> foo a b1 = foo a b2 $`
--| * `fooeq1d: $ G -> a1 = a2 $ > $ G -> foo a1 b = foo a2 b $`
--| * `fooeq2: $ G -> b1 = b2 $ > $ G -> foo a b1 = foo a b2 $`
--|
--| for any definition `foo`.
(def (add-eqN-thms t . args)
(def idx (ref! 0))
(def base (get-tgt-args args t "eq"))
@ match (make-eqNd-thms t)
[(and (__ 2) thms)
@ scan thms @ match-fn @ (bis hs ret val)
(set! idx {idx + 1})
(def tgt (atom-app base idx "d"))
@ if (undef? (get-decl tgt)) @ begin
(add-thm! tgt bis hs ret () '(() ,val))
(def tgt2 (atom-app base idx))
@ if (undef? (get-decl tgt2)) @ begin
@ match (ded-to-thm tgt) [#undef] @ (bis2 ret2 val2)
(add-thm! tgt2 bis2 () ret2 () val2)]
[_])
(def derive-eq @ match-fn*
[(t1 t2 t3) @ fn (s)
(add-eqd-thm s '',t1)
(add-eq-thm s '',t2)
(add-eqN-thms s '',t3)]
[args @ fn (s)
(apply add-eqd-thm s args)
(apply add-eq-thm s args)
(apply add-eqN-thms s args)])
(def eval-map (atom-map!
'[im ,(fn (a b) {(not (eval a)) or (eval b)})]
'[not ,(fn (a) (not (eval a)))]))
(set-merge-strategy eval-map merge-map)
(def (eval e) @ match e @ ((? atom? t) . es)
(apply
(lookup eval-map t @ fn () @ error
@ string-append "unknown function encountered during evaluation: " (->string t))
es))
--| This is used as an annotation.
--| * `@(add-eval f) def foo ..` will add `f` as an evaluator for `foo`,
--| which is used by the `eval` function (which can evaluate many
--| closed terms of sort `nat` or `wff` to values).
--| * `@(add-eval)` will attempt to evaluate the body of the definition
--| and use that as the result.
(def ((add-eval . f) a)
(if (def? @ lookup eval-map a) (error "already defined evaluation rule"))
@ insert! eval-map a @ match f
[(f) (if (fn? f) f (fn () f))]
[() (def x @ eval @ nth 6 @ get-decl a) (fn () x)])
--| `@eval-check` is an annotation that can be placed on theorems or axioms which
--| are closed terms, and will check that the theorem/axiom evaluates to `#t`.
--| This is not formally rigorous as the evaluator is not verified, but it can be
--| viewed as a cross-check of the axiom or the evaluator, depending on your
--| point of view.
(def (eval-check a) @ match (eval @ nth 4 @ get-decl a) [#t])
};
-- configuration
do {
(set-timeout 500)
(def (refine-extra-args refine tgt e . ps)
@ refine tgt (foldl ps (verb e) @ fn (acc p2) @ copy-span e '(ax_mp ,acc ,p2)))
(def default-annotate (derive-eq))
(def (annotate e s) @ match e ['_ (default-annotate s)] [_ (e s)])
};
theorem a1i (h: $ b $): $ a -> b $ = '(ax_1 h);
theorem a2i (h: $ a -> b -> c $): $ (a -> b) -> (a -> c) $ = '(ax_2 h);
theorem mpd (h1: $ a -> b $) (h2: $ a -> b -> c $): $ a -> c $ = '(ax_2 h2 h1);
theorem mpi (h1: $ b $) (h2: $ a -> b -> c $): $ a -> c $ = '(mpd (a1i h1) h2);
theorem id: $ a -> a $ = '(mpd (! ax_1 _ a) ax_1);
theorem idd: $ a -> b -> b $ = '(a1i id);
theorem syl (h1: $ b -> c $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (a1i h1));
theorem rsyl (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 h1);
theorem a1d (h: $ a -> b $): $ a -> c -> b $ = '(syl ax_1 h);
theorem a2d (h: $ a -> b -> c -> d $): $ a -> (b -> c) -> (b -> d) $ = '(syl ax_2 h);
theorem a3d (h: $ a -> ~b -> ~c $): $ a -> c -> b $ = '(syl ax_3 h);
theorem sylc (h: $ b -> c -> d $) (h1: $ a -> b $) (h2: $ a -> c $): $ a -> d $ = '(mpd h2 @ syl h h1);
theorem syld (h1: $ a -> b -> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(mpd h1 @ a2d @ a1d h2);
theorem syl5 (h1: $ b -> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (a1i h1) h2);
theorem syl6 (h1: $ c -> d $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syld h2 (a1i h1));
theorem imim2: $ (b -> c) -> (a -> b) -> (a -> c) $ = '(a2d ax_1);
theorem imim2i (h: $ b -> c $): $ (a -> b) -> (a -> c) $ = '(imim2 h);
theorem imim2d (h: $ a -> c -> d $): $ a -> (b -> c) -> (b -> d) $ = '(syl imim2 h);
theorem absurd: $ ~a -> a -> b $ = '(a3d ax_1);
theorem com12 (h: $ a -> b -> c $): $ b -> a -> c $ = '(syl (a2i h) ax_1);
theorem mpcom: $ a -> (a -> b) -> b $ = '(com12 id);
theorem com23 (h: $ a -> b -> c -> d $): $ a -> c -> b -> d $ = '(syl (com12 @ imim2d mpcom) h);
theorem eimd (h1: $ a -> b $) (h2: $ a -> c -> d $): $ a -> (b -> c) -> d $ = '(syld (rsyl h1 mpcom) h2);
theorem absurdr: $ a -> ~a -> b $ = '(com12 absurd);
theorem imim1: $ (a -> b) -> (b -> c) -> (a -> c) $ = '(com12 imim2);
theorem imim1i (h: $ a -> b $): $ (b -> c) -> (a -> c) $ = '(imim1 h);
theorem imim1d (h: $ a -> b -> c $): $ a -> (c -> d) -> (b -> d) $ = '(syl imim1 h);
theorem imimd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $):
$ a -> (c -> d) -> (b -> e) $ = '(syld (imim1d h1) (imim2d h2));
theorem imim: $ (a -> b) -> (c -> d) -> (b -> c) -> (a -> d) $ = '(syl5 imim2 (imim2d imim1));
theorem imidm: $ (a -> a -> b) -> a -> b $ = '(a2i mpcom);
theorem eim: $ a -> (b -> c) -> (a -> b) -> c $ = '(imim1d mpcom);
theorem contra: $ (~a -> a) -> a $ = '(imidm (a3d (a2i absurd)));
theorem dne: $ ~~a -> a $ = '(syl contra absurd);
theorem inot: $ (a -> ~a) -> ~a $ = '(syl contra (imim1 dne));
theorem con2: $ (a -> ~b) -> (b -> ~a) $ = '(a3d (syl5 dne id));
theorem notnot1: $ a -> ~~a $ = '(con2 id);
theorem con3: $ (a -> b) -> (~b -> ~a) $ = '(syl con2 (imim2i notnot1));
theorem con1: $ (~a -> b) -> (~b -> a) $ = '(a3d (imim2i notnot1));
theorem cases (h1: $ a -> b $) (h2: $ ~a -> b $): $ b $ = '(contra @ syl h1 @ con1 h2);
theorem casesd (h1: $ a -> b -> c $) (h2: $ a -> ~b -> c $): $ a -> c $ =
'(cases (com12 h1) (com12 h2));
theorem con1d (h: $ a -> ~b -> c $): $ a -> ~c -> b $ = '(syl con1 h);
theorem con2d (h: $ a -> b -> ~c $): $ a -> c -> ~b $ = '(syl con2 h);
theorem con3d (h: $ a -> b -> c $): $ a -> ~c -> ~b $ = '(syl con3 h);
theorem con4d (h: $ a -> ~b -> ~c $): $ a -> c -> b $ = '(syl ax_3 h);
theorem mt (h1: $ b -> a $) (h2: $ ~a $): $ ~b $ = '(con3 h1 h2);
theorem mt2 (h1: $ b -> ~a $) (h2: $ a $): $ ~b $ = '(con2 h1 h2);
theorem mtd (h1: $ a -> ~b $) (h2: $ a -> c -> b $): $ a -> ~c $ = '(mpd h1 (con3d h2));
theorem mti (h1: $ ~b $) (h2: $ a -> c -> b $): $ a -> ~c $ = '(mtd (a1i h1) h2);
theorem mt2d (h1: $ a -> c $) (h2: $ a -> b -> ~c $): $ a -> ~b $ = '(sylc con2 h2 h1);
--| Conjunction: `a` and `b` are both true.
@(add-eval @ fn (a b) {(eval a) and (eval b)})
def an (a b: wff): wff = $ ~(a -> ~b) $;
infixl an: $/\$ prec 34;
theorem anl: $ a /\ b -> a $ = '(con1 absurd);
theorem anr: $ a /\ b -> b $ = '(con1 ax_1);
theorem anli (h: $ a /\ b $): $ a $ = '(anl h);
theorem anri (h: $ a /\ b $): $ b $ = '(anr h);
theorem ian: $ a -> b -> a /\ b $ = '(con2d mpcom);
theorem iand (h1: $ a -> b $) (h2: $ a -> c $): $ a -> b /\ c $ = '(sylc ian h1 h2);
theorem anld (h: $ a -> b /\ c $): $ a -> b $ = '(syl anl h);
theorem anrd (h: $ a -> b /\ c $): $ a -> c $ = '(syl anr h);
theorem iani (h1: $ a $) (h2: $ b $): $ a /\ b $ = '(ian h1 h2);
theorem anwl (h: $ a -> c $): $ a /\ b -> c $ = '(syl h anl);
theorem anwr (h: $ b -> c $): $ a /\ b -> c $ = '(syl h anr);
theorem anll: $ a /\ b /\ c -> a $ = '(anwl anl);
theorem anlr: $ a /\ b /\ c -> b $ = '(anwl anr);
theorem anrl: $ a /\ (b /\ c) -> b $ = '(anwr anl);
theorem anrr: $ a /\ (b /\ c) -> c $ = '(anwr anr);
theorem anwll (h: $ a -> d $): $ a /\ b /\ c -> d $ = '(anwl (anwl h));
theorem anw3l (h: $ a -> e $): $ a /\ b /\ c /\ d -> e $ = '(anwll (anwl h));
theorem anw4l (h: $ a -> f $): $ a /\ b /\ c /\ d /\ e -> f $ = '(anw3l (anwl h));
theorem anw5l (h: $ a -> g $): $ a /\ b /\ c /\ d /\ e /\ f -> g $ = '(anw4l (anwl h));
theorem anw6l (x: $ a -> h $): $ a /\ b /\ c /\ d /\ e /\ f /\ g -> h $ = '(anw5l (anwl x));
theorem anw7l (x: $ a -> i $): $ a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> i $ = '(anw6l (anwl x));
theorem anllr: $ a /\ b /\ c /\ d -> b $ = '(anwll anr);
theorem an3l: $ a /\ b /\ c /\ d -> a $ = '(anwll anl);
theorem an3lr: $ a /\ b /\ c /\ d /\ e -> b $ = '(anwl anllr);
theorem an4l: $ a /\ b /\ c /\ d /\ e -> a $ = '(anwl an3l); -- TODO: automate these
theorem an4lr: $ a /\ b /\ c /\ d /\ e /\ f -> b $ = '(anwl an3lr);
theorem an5l: $ a /\ b /\ c /\ d /\ e /\ f -> a $ = '(anwl an4l);
theorem an5lr: $ a /\ b /\ c /\ d /\ e /\ f /\ g -> b $ = '(anwl an4lr);
theorem an6l: $ a /\ b /\ c /\ d /\ e /\ f /\ g -> a $ = '(anwl an5l);
theorem an6lr: $ a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> b $ = '(anwl an5lr);
theorem imp (h: $ a -> b -> c $): $ a /\ b -> c $ = '(sylc h anl anr);
theorem exp (h: $ a /\ b -> c $): $ a -> b -> c $ = '(syl6 h ian);
theorem impcom (h: $ a -> b -> c $): $ b /\ a -> c $ = '(imp (com12 h));
theorem expcom (h: $ a /\ b -> c $): $ b -> a -> c $ = '(com12 (exp h));
theorem syla (h1: $ (b -> c) -> d $) (h2: $ a /\ b -> c $): $ a -> d $ = '(syl h1 @ exp h2);
theorem sylan (h: $ b /\ c -> d $) (h1: $ a -> b $) (h2: $ a -> c $):
$ a -> d $ = '(syl h @ iand h1 h2);
theorem animd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $): $ a -> b /\ d -> c /\ e $ =
'(exp (iand (imp (syl5 anl h1)) (imp (syl5 anr h2))));
theorem anim1d (h: $ a -> b -> c $): $ a -> b /\ d -> c /\ d $ = '(animd h idd);
theorem anim2d (h: $ a -> c -> d $): $ a -> b /\ c -> b /\ d $ = '(animd idd h);
theorem anim1: $ (a -> b) -> a /\ c -> b /\ c $ = '(anim1d id);
theorem anim2: $ (b -> c) -> a /\ b -> a /\ c $ = '(anim2d id);
theorem anim: $ (a -> b) -> (c -> d) -> a /\ c -> b /\ d $ =
'(exp @ syld (anim1d anl) (anim2d anr));
theorem anim2a: $ (a -> b -> c) -> (a /\ b -> a /\ c) $ =
'(exp @ iand anrl @ mpd anrr @ mpd anrl anl);
theorem ancom: $ a /\ b -> b /\ a $ = '(iand anr anl);
theorem anrasss (h: $ a /\ b /\ c -> d $): $ a /\ c /\ b -> d $ =
'(sylan h (iand anll anr) anlr);
theorem anim1a: $ (a -> b -> c) -> (b /\ a -> c /\ a) $ =
'(syl6 ancom @ syl5 ancom anim2a);
theorem casesda (h1: $ a /\ b -> c $) (h2: $ a /\ ~b -> c $): $ a -> c $ =
'(casesd (exp h1) (exp h2));
theorem inotda (h: $ a /\ b -> ~b $): $ a -> ~b $ = '(syla inot h);
theorem mpand (h1: $ a -> b $) (h2: $ a /\ b -> c $): $ a -> c $ = '(mpd h1 (exp h2));
theorem mtand (h1: $ a -> ~b $) (h2: $ a /\ c -> b $): $ a -> ~c $ = '(mtd h1 (exp h2));
theorem mtani (h1: $ ~b $) (h2: $ a /\ c -> b $): $ a -> ~c $ = '(mtand (a1i h1) h2);
--| If and only if: `a` implies `b`, and `b` implies `a`.
@(add-eval @ fn (a b) {(eval a) == (eval b)})
def iff (a b: wff): wff = $ (a -> b) /\ (b -> a) $;
infixl iff: $<->$ prec 20;
theorem bi1: $ (a <-> b) -> a -> b $ = 'anl;
theorem bi1i (h: $ a <-> b $): $ a -> b $ = '(bi1 h);
theorem bi1d (h: $ a -> (b <-> c) $): $ a -> b -> c $ = '(syl bi1 h);
theorem bi1a (h: $ a -> (b <-> c) $): $ a /\ b -> c $ = '(imp @ bi1d h);
theorem bi2: $ (a <-> b) -> b -> a $ = 'anr;
theorem bi2i (h: $ a <-> b $): $ b -> a $ = '(bi2 h);
theorem bi2d (h: $ a -> (b <-> c) $): $ a -> c -> b $ = '(syl bi2 h);
theorem bi2a (h: $ a -> (b <-> c) $): $ a /\ c -> b $ = '(imp @ bi2d h);
theorem ibii (h1: $ a -> b $) (h2: $ b -> a $): $ a <-> b $ = '(iani h1 h2);
theorem ibid (h1: $ a -> b -> c $) (h2: $ a -> c -> b $): $ a -> (b <-> c) $ = '(iand h1 h2);
theorem ibida (h1: $ a /\ b -> c $) (h2: $ a /\ c -> b $): $ a -> (b <-> c) $ = '(ibid (exp h1) (exp h2));
theorem biid: $ a <-> a $ = '(ibii id id);
theorem biidd: $ a -> (b <-> b) $ = '(a1i biid);
theorem mpbi (h1: $ a <-> b $) (h2: $ a $): $ b $ = '(bi1i h1 h2);
theorem mpbir (h1: $ b <-> a $) (h2: $ a $): $ b $ = '(bi2i h1 h2);
theorem mpbid (h1: $ a -> (b <-> c) $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (bi1d h1));
theorem mpbird (h1: $ a -> (c <-> b) $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (bi2d h1));
theorem mpbii (h1: $ b $) (h2: $ a -> (b <-> c) $): $ a -> c $ = '(mpbid h2 (a1i h1));
theorem mpbiri (h1: $ b $) (h2: $ a -> (c <-> b) $): $ a -> c $ = '(mpbird h2 (a1i h1));
theorem mtbi (h1: $ a <-> b $) (h2: $ ~a $): $ ~b $ = '(mt (bi2 h1) h2);
theorem mtbir (h1: $ b <-> a $) (h2: $ ~a $): $ ~b $ = '(mt (bi1 h1) h2);
theorem mtbid (h1: $ a -> (b <-> c) $) (h2: $ a -> ~b $): $ a -> ~c $ = '(mtd h2 (bi2d h1));
theorem mtbird (h1: $ a -> (c <-> b) $) (h2: $ a -> ~b $): $ a -> ~c $ = '(mtd h2 (bi1d h1));
theorem con1b: $ (~a <-> b) -> (~b <-> a) $ = '(ibid (con1d bi1) (con2d bi2));
theorem con2b: $ (a <-> ~b) -> (b <-> ~a) $ = '(ibid (con2d bi1) (con1d bi2));
theorem con3b: $ (a <-> b) -> (~a <-> ~b) $ = '(ibid (con3d bi2) (con3d bi1));
theorem con4b: $ (~a <-> ~b) -> (a <-> b) $ = '(ibid (con4d bi2) (con4d bi1));
theorem con1bb: $ (~a <-> b) <-> (~b <-> a) $ = '(ibii con1b con1b);
theorem con2bb: $ (a <-> ~b) <-> (b <-> ~a) $ = '(ibii con2b con2b);
theorem con3bb: $ (a <-> b) <-> (~a <-> ~b) $ = '(ibii con3b con4b);
theorem con1bi: $ (~a -> b) <-> (~b -> a) $ = '(ibii con1 con1);
theorem con2bi: $ (a -> ~b) <-> (b -> ~a) $ = '(ibii con2 con2);
theorem con3bi: $ (a -> b) <-> (~b -> ~a) $ = '(ibii con3 ax_3);
theorem notnot: $ a <-> ~~a $ = '(ibii notnot1 dne);
theorem bithd (h1: $ a -> b $) (h2: $ a -> c $): $ a -> (b <-> c) $ = '(ibid (a1d h2) (a1d h1));
theorem binthd (h1: $ a -> ~b $) (h2: $ a -> ~c $): $ a -> (b <-> c) $ = '(syl con4b @ bithd h1 h2);
theorem bith: $ a -> b -> (a <-> b) $ = '(exp @ bithd anl anr);
theorem binth: $ ~a -> ~b -> (a <-> b) $ = '(exp @ binthd anl anr);
theorem bicom: $ (a <-> b) -> (b <-> a) $ = '(ibid bi2 bi1);
theorem bicomb: $ (a <-> b) <-> (b <-> a) $ = '(ibii bicom bicom);
theorem bicomd (h: $ a -> (b <-> c) $): $ a -> (c <-> b) $ = '(syl bicom h);
theorem bitrd (h1: $ a -> (b <-> c) $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ =
'(ibid (syld (bi1d h1) (bi1d h2)) (syld (bi2d h2) (bi2d h1)));
theorem bitr2d (h1: $ a -> (b <-> c) $) (h2: $ a -> (c <-> d) $): $ a -> (d <-> b) $ = '(bicomd (bitrd h1 h2));
theorem bitr3d (h1: $ a -> (c <-> b) $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(bitrd (bicomd h1) h2);
theorem bitr4d (h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> c) $): $ a -> (b <-> d) $ = '(bitrd h1 (bicomd h2));
theorem bitr: $ (a <-> b) -> (b <-> c) -> (a <-> c) $ = '(exp (bitrd anl anr));
theorem bitr2: $ (a <-> b) -> (b <-> c) -> (c <-> a) $ = '(exp (bitr2d anl anr));
theorem bitr3: $ (b <-> a) -> (b <-> c) -> (a <-> c) $ = '(exp (bitr3d anl anr));
theorem bitr4: $ (a <-> b) -> (c <-> b) -> (a <-> c) $ = '(exp (bitr4d anl anr));
theorem sylib (h1: $ b <-> c $) (h2: $ a -> b $): $ a -> c $ = '(syl (bi1i h1) h2);
theorem sylibr (h1: $ c <-> b $) (h2: $ a -> b $): $ a -> c $ = '(syl (bi2i h1) h2);
theorem sylbi (h1: $ a <-> b $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 (bi1i h1));
theorem sylbir (h1: $ b <-> a $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 (bi2i h1));
theorem syl5bb (h1: $ b <-> c $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(bitrd (a1i h1) h2);
theorem syl5bbr (h1: $ c <-> b $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(syl5bb (bicom h1) h2);
theorem syl6bb (h1: $ c <-> d $) (h2: $ a -> (b <-> c) $): $ a -> (b <-> d) $ = '(bitrd h2 (a1i h1));
theorem syl6bbr (h1: $ d <-> c $) (h2: $ a -> (b <-> c) $): $ a -> (b <-> d) $ = '(syl6bb (bicom h1) h2);
theorem syl5bi (h1: $ b <-> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syl5 (bi1 h1) h2);
theorem syl5bir (h1: $ c <-> b $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syl5bi (bicom h1) h2);
theorem syl6ib (h1: $ c <-> d $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syl6 (bi1 h1) h2);
theorem syl6ibr (h1: $ d <-> c $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syl6 (bi2 h1) h2);
theorem syl5ibrcom (h1: $ c -> (b <-> d) $) (h2: $ a -> d $): $ a -> c -> b $ = '(com12 @ syl5 h2 (bi2d h1));
theorem sylbid (h1: $ a -> (b <-> c) $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (bi1d h1) h2);
theorem sylibd (h1: $ a -> b -> c $) (h2: $ a -> (c <-> d) $): $ a -> b -> d $ = '(syld h1 (bi1d h2));
theorem sylbird (h1: $ a -> (c <-> b) $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (bi2d h1) h2);
theorem sylibrd (h1: $ a -> b -> c $) (h2: $ a -> (d <-> c) $): $ a -> b -> d $ = '(syld h1 (bi2d h2));
theorem bitr3g (h1: $ b <-> d $) (h2: $ c <-> e $) (h: $ a -> (b <-> c) $):
$ a -> (d <-> e) $ = '(syl5bb (bicom h1) @ syl6bb h2 h);
theorem bitr4g (h1: $ d <-> b $) (h2: $ e <-> c $) (h: $ a -> (b <-> c) $):
$ a -> (d <-> e) $ = '(syl5bb h1 @ syl6bb (bicom h2) h);
theorem bitr3gi (h1: $ a <-> c $) (h2: $ b <-> d $) (h: $ a <-> b $): $ c <-> d $ = '(bitr3 h1 @ bitr h h2);
theorem bitr4gi (h1: $ c <-> a $) (h2: $ d <-> b $) (h: $ a <-> b $): $ c <-> d $ = '(bitr h1 @ bitr4 h h2);
theorem impbi (h: $ a -> (b <-> c) $): $ a /\ b -> c $ = '(imp @ bi1d h);
theorem impbir (h: $ a -> (c <-> b) $): $ a /\ b -> c $ = '(imp @ bi2d h);
theorem ancomb: $ a /\ b <-> b /\ a $ = '(ibii ancom ancom);
theorem anass: $ a /\ b /\ c <-> a /\ (b /\ c) $ =
'(ibii (iand anll (anim1 anr)) (iand (anim2 anl) anrr));
theorem bian2a: $ (a -> b) -> (a /\ b <-> a) $ = '(ibid (a1i anl) (a2i ian));
theorem bian1a: $ (b -> a) -> (a /\ b <-> b) $ = '(syl5bb ancomb bian2a);
theorem bian1: $ a -> (a /\ b <-> b) $ = '(syl bian1a ax_1);
theorem bian2: $ b -> (a /\ b <-> a) $ = '(syl bian2a ax_1);
theorem bibi1: $ a -> ((a <-> b) <-> b) $ = '(ibid (com12 bi1) bith);
theorem bibi2: $ b -> ((a <-> b) <-> a) $ = '(syl5bb bicomb bibi1);
theorem noteq: $ (a <-> b) -> (~a <-> ~b) $ = 'con3b;
theorem noteqi (h: $ a <-> b $): $ ~a <-> ~b $ = '(noteq h);
@(register-eqd 'not) theorem noteqd (h: $ a -> (b <-> c) $): $ a -> (~b <-> ~c) $ = '(syl noteq h);
@(register-eqd 'im) theorem imeqd
(h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> (b -> d <-> c -> e) $ =
'(ibid (imimd (bi2d h1) (bi1d h2)) (imimd (bi1d h1) (bi2d h2)));
theorem bibin1: $ ~a -> ((a <-> b) <-> ~b) $ = '(ibid (com12 @ bi1d noteq) binth);
theorem bibin2: $ ~b -> ((a <-> b) <-> ~a) $ = '(syl5bb bicomb bibin1);
theorem imeq1d (h: $ a -> (b <-> c) $): $ a -> (b -> d <-> c -> d) $ = '(imeqd h biidd);
theorem imeq2d (h: $ a -> (c <-> d) $): $ a -> (b -> c <-> b -> d) $ = '(imeqd biidd h);
theorem imeq1i (h: $ a <-> b $): $ a -> c <-> b -> c $ = '(imeq1d id h);
theorem imeq2i (h: $ b <-> c $): $ a -> b <-> a -> c $ = '(imeq2d id h);
theorem imeqi (h1: $ a <-> b $) (h2: $ c <-> d $): $ a -> c <-> b -> d $ = '(bitr (imeq1i h1) (imeq2i h2));
@(register-eqd 'an) theorem aneqd
(h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> (b /\ d <-> c /\ e) $ =
'(ibid (animd (bi1d h1) (bi1d h2)) (animd (bi2d h1) (bi2d h2)));
theorem imeq2a: $ (a -> (b <-> c)) -> (a -> b <-> a -> c) $ = '(ibid (a2d @ imim2i bi1) (a2d @ imim2i bi2));
theorem imeq1a: $ (~c -> (a <-> b)) -> (a -> c <-> b -> c) $ = '(bitr4g con3bi con3bi @ syl imeq2a @ imim2i noteq);
theorem imeq2da (h: $ G /\ a -> (b <-> c) $): $ G -> (a -> b <-> a -> c) $ = '(syl imeq2a @ exp h);
theorem aneq1d (h: $ a -> (b <-> c) $): $ a -> (b /\ d <-> c /\ d) $ = '(aneqd h biidd);
theorem aneq2d (h: $ a -> (c <-> d) $): $ a -> (b /\ c <-> b /\ d) $ = '(aneqd biidd h);
theorem aneq: $ (a <-> b) -> (c <-> d) -> (a /\ c <-> b /\ d) $ = '(exp @ aneqd anl anr);
theorem aneq1i (h: $ a <-> b $): $ a /\ c <-> b /\ c $ = '(aneq1d id h);
theorem aneq2i (h: $ b <-> c $): $ a /\ b <-> a /\ c $ = '(aneq2d id h);
theorem aneq2a: $ (a -> (b <-> c)) -> (a /\ b <-> a /\ c) $ =
'(ibid (syl anim2a @ imim2i bi1) (syl anim2a @ imim2i bi2));
theorem aneq1a: $ (c -> (a <-> b)) -> (a /\ c <-> b /\ c) $ = '(syl5bb ancomb @ syl6bb ancomb aneq2a);
theorem aneq1da (h: $ G /\ c -> (a <-> b) $): $ G -> (a /\ c <-> b /\ c) $ = '(syl aneq1a @ exp h);
theorem aneq2da (h: $ G /\ a -> (b <-> c) $): $ G -> (a /\ b <-> a /\ c) $ = '(syl aneq2a @ exp h);
theorem anlass: $ a /\ (b /\ c) <-> b /\ (a /\ c) $ =
'(bitr3 anass @ bitr (aneq1i ancomb) anass);
theorem anrass: $ a /\ b /\ c <-> a /\ c /\ b $ =
'(bitr anass @ bitr4 (aneq2i ancomb) anass);
theorem an4: $ (a /\ b) /\ (c /\ d) <-> (a /\ c) /\ (b /\ d) $ =
'(bitr4 anass @ bitr4 anass @ aneq2i anlass);
theorem anroti (h: $ a -> b /\ d $): $ a /\ c -> b /\ c /\ d $ = '(sylib anrass @ anim1 h);
theorem anrotri (h: $ b /\ d -> a $): $ b /\ c /\ d -> a /\ c $ = '(sylbi anrass @ anim1 h);
theorem bian11i (h: $ a <-> b /\ c $): $ a /\ d <-> b /\ (c /\ d) $ = '(bitr (aneq1i h) anass);
theorem bian21i (h: $ a <-> b /\ c $): $ a /\ d <-> (b /\ d) /\ c $ = '(bitr (aneq1i h) anrass);
theorem bian12i (h: $ a <-> b /\ c $): $ d /\ a <-> b /\ (d /\ c) $ = '(bitr (aneq2i h) anlass);
theorem bian22i (h: $ a <-> b /\ c $): $ d /\ a <-> (d /\ b) /\ c $ = '(bitr4 (aneq2i h) anass);
theorem bian11d (h: $ G -> (a <-> b /\ c) $): $ G -> (a /\ d <-> b /\ (c /\ d)) $ = '(syl6bb anass (aneq1d h));
theorem bian21d (h: $ G -> (a <-> b /\ c) $): $ G -> (a /\ d <-> (b /\ d) /\ c) $ = '(syl6bb anrass (aneq1d h));
theorem bian12d (h: $ G -> (a <-> b /\ c) $): $ G -> (d /\ a <-> b /\ (d /\ c)) $ = '(syl6bb anlass (aneq2d h));
theorem bian22d (h: $ G -> (a <-> b /\ c) $): $ G -> (d /\ a <-> (d /\ b) /\ c) $ = '(syl6bbr anass (aneq2d h));
theorem bian11da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (a /\ d <-> b /\ (c /\ d)) $ = '(syl6bb anass (aneq1da h));
theorem bian21da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (a /\ d <-> (b /\ d) /\ c) $ = '(syl6bb anrass (aneq1da h));
theorem bian12da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (d /\ a <-> b /\ (d /\ c)) $ = '(syl6bb anlass (aneq2da h));
theorem bian22da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (d /\ a <-> (d /\ b) /\ c) $ = '(syl6bbr anass (aneq2da h));
theorem anidm: $ a /\ a <-> a $ = '(ibii anl (iand id id));
theorem anandi: $ a /\ (b /\ c) <-> (a /\ b) /\ (a /\ c) $ = '(bitr3 (aneq1i anidm) an4);
theorem anandir: $ (a /\ b) /\ c <-> (a /\ c) /\ (b /\ c) $ = '(bitr3 (aneq2i anidm) an4);
theorem imandi: $ (a -> b /\ c) <-> (a -> b) /\ (a -> c) $ =
'(ibii (iand (imim2i anl) (imim2i anr)) (com12 @ animd mpcom mpcom));
theorem imancom: $ a /\ (b -> c) -> b -> a /\ c $ = '(com12 @ anim2d mpcom);
theorem rbida (h1: $ a /\ c -> b $) (h2: $ a /\ d -> b $)
(h: $ a /\ b -> (c <-> d) $): $ a -> (c <-> d) $ =
'(bitr3d (syla bian2a h1) @ bitrd (syla aneq1a h) (syla bian2a h2));
theorem rbid (h1: $ b -> a $) (h2: $ c -> a $) (h: $ a -> (b <-> c) $): $ b <-> c $ =
'(bitr3 (bian2a h1) @ bitr (aneq1a h) (bian2a h2));
@(register-eqd 'iff) theorem bieqd
(h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> ((b <-> d) <-> (c <-> e)) $ =
'(aneqd (imeqd h1 h2) (imeqd h2 h1));
theorem bieq1d (h: $ a -> (b <-> c) $): $ a -> ((b <-> d) <-> (c <-> d)) $ = '(bieqd h biidd);
theorem bieq2d (h: $ a -> (c <-> d) $): $ a -> ((b <-> c) <-> (b <-> d)) $ = '(bieqd biidd h);
theorem bieq: $ (a <-> b) -> (c <-> d) -> ((a <-> c) <-> (b <-> d)) $ = '(exp (bieqd anl anr));
theorem bieq1: $ (a <-> b) -> ((a <-> c) <-> (b <-> c)) $ = '(bieq1d id);
theorem bieq2: $ (b <-> c) -> ((a <-> b) <-> (a <-> c)) $ = '(bieq2d id);
theorem impexp: $ (a /\ b -> c) <-> (a -> b -> c) $ =
'(ibii (exp @ exp @ mpd (anim1 anr) anll) (exp @ mpd anrr @ mpd anrl anl));
theorem impd (h: $ a -> b -> c -> d $): $ a -> b /\ c -> d $ = '(sylibr impexp h);
theorem expd (h: $ a -> b /\ c -> d $): $ a -> b -> c -> d $ = '(sylib impexp h);
theorem com12b: $ (a -> b -> c) <-> (b -> a -> c) $ = '(ibii (com23 id) (com23 id));
--| Disjunction: either `a` is true or `b` is true.
@(add-eval @ fn (a b) {(eval a) or (eval b)})
@_ def or (a b: wff): wff = $ ~a -> b $;
infixl or: $\/$ prec 30;
theorem orl: $ a -> a \/ b $ = 'absurdr;
theorem orr: $ b -> a \/ b $ = 'ax_1;
theorem eori (h1: $ a -> c $) (h2: $ b -> c $): $ a \/ b -> c $ =
'(casesd (a1i h1) (imim2i h2));
theorem eord (h1: $ a -> b -> d $) (h2: $ a -> c -> d $):
$ a -> b \/ c -> d $ = '(com12 (eori (com12 h1) (com12 h2)));
theorem eorda (h1: $ a /\ b -> d $) (h2: $ a /\ c -> d $):
$ a -> b \/ c -> d $ = '(eord (exp h1) (exp h2));
theorem orld (h: $ a -> b $): $ a -> b \/ c $ = '(syl orl h);
theorem orrd (h: $ a -> c $): $ a -> b \/ c $ = '(syl orr h);
theorem eor: $ (a -> c) -> (b -> c) -> a \/ b -> c $ = '(exp (eord anl anr));
theorem orimd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $): $ a -> b \/ d -> c \/ e $ =
'(eord (syl6 orl h1) (syl6 orr h2));
theorem orim1d (h: $ a -> b -> c $): $ a -> b \/ d -> c \/ d $ = '(orimd h idd);
theorem orim2d (h: $ a -> c -> d $): $ a -> b \/ c -> b \/ d $ = '(orimd idd h);
theorem orim1: $ (a -> b) -> a \/ c -> b \/ c $ = '(orim1d id);
theorem orim2: $ (b -> c) -> a \/ b -> a \/ c $ = '(orim2d id);
theorem oreq1i (h: $ a <-> b $): $ a \/ c <-> b \/ c $ = '(oreq1d id h);
theorem oreq2i (h: $ b <-> c $): $ a \/ b <-> a \/ c $ = '(oreq2d id h);
theorem orim: $ (a -> b) -> (c -> d) -> a \/ c -> b \/ d $ = '(exp @ syld (anwl orim1) (anwr orim2));
theorem oreqi (h1: $ a <-> b $) (h2: $ c <-> d $): $ a \/ c <-> b \/ d $ = '(bitr (oreq1i h1) (oreq2i h2));
theorem orcom: $ a \/ b -> b \/ a $ = 'con1;
theorem orcomb: $ a \/ b <-> b \/ a $ = '(ibii orcom orcom);
theorem or12: $ a \/ (b \/ c) <-> b \/ (a \/ c) $ = '(bitr3 impexp @ bitr (imeq1i ancomb) impexp);
theorem orass: $ a \/ b \/ c <-> a \/ (b \/ c) $ = '(bitr orcomb @ bitr or12 (oreq2 orcomb));
theorem or4: $ (a \/ b) \/ (c \/ d) <-> (a \/ c) \/ (b \/ d) $ = '(bitr4 orass @ bitr4 orass @ oreq2 or12);
theorem oridm: $ a \/ a <-> a $ = '(ibii (eor id id) orl);
theorem notan2: $ ~(a /\ b) <-> a -> ~b $ = '(bicom notnot);
theorem notan: $ ~(a /\ b) <-> (~a \/ ~b) $ = '(bitr notan2 (imeq1i notnot));
theorem notor: $ ~(a \/ b) <-> (~a /\ ~b) $ = '(con1b (bitr4 notan (oreqi notnot notnot)));
theorem iman: $ a -> b <-> ~(a /\ ~b) $ = '(bitr4 (imeq2i notnot) notan2);
theorem imor: $ ((a \/ b) -> c) <-> ((a -> c) /\ (b -> c)) $ =
'(ibii (iand (imim1i orl) (imim1i orr)) (imp eor));
theorem andi: $ a /\ (b \/ c) <-> a /\ b \/ a /\ c $ =
'(ibii (imp @ orimd ian ian) @ eor (anim2 orl) (anim2 orr));
theorem andir: $ (a \/ b) /\ c <-> a /\ c \/ b /\ c $ =
'(bitr ancomb @ bitr andi @ oreqi ancomb ancomb);
theorem ordi: $ a \/ (b /\ c) <-> (a \/ b) /\ (a \/ c) $ =
'(ibii (iand (orim2 anl) (orim2 anr)) @ com12 @ animd mpcom mpcom);
theorem ordir: $ (a /\ b) \/ c <-> (a \/ c) /\ (b \/ c) $ =
'(bitr orcomb @ bitr ordi @ aneq orcomb orcomb);
theorem oreq2a: $ (~a -> (b <-> c)) -> (a \/ b <-> a \/ c) $ = 'imeq2a;
theorem oreq1a: $ (~c -> (a <-> b)) -> (a \/ c <-> b \/ c) $ = '(syl5bb orcomb @ syl6bb orcomb oreq2a);
theorem biim1a: $ (~a -> b) -> (a -> b <-> b) $ = '(ibid (exp @ casesd anr anl) (a1i ax_1));
theorem biim2a: $ (b -> ~a) -> (a -> b <-> ~a) $ = '(ibid (exp @ syl inot @ imp imim2) (a1i absurd));
theorem bior1a: $ (a -> b) -> (a \/ b <-> b) $ = '(sylbi (imeq1i notnot) biim1a);
theorem bior2a: $ (b -> a) -> (a \/ b <-> a) $ = '(syl5bb orcomb bior1a);
theorem biim1: $ a -> (a -> b <-> b) $ = '(syl biim1a absurdr);
theorem biim2: $ ~b -> (a -> b <-> ~a) $ = '(syl biim2a absurd);
theorem bior1: $ ~a -> (a \/ b <-> b) $ = '(syl bior1a absurd);
theorem bior2: $ ~b -> (a \/ b <-> a) $ = '(syl bior2a absurd);
theorem em: $ p \/ ~p $ = 'id;
theorem emr: $ ~p \/ p $ = '(orcom em);
--| Selection: `ifp p a b` is equivalent to `a` if `p` is true,
--| and equivalent to `b` if `p` is false.
@(add-eval @ fn (a b c) (if (eval a) (eval b) (eval c)))
@_ abstract def ifp (p a b: wff): wff = $ p /\ a \/ ~p /\ b $;
pub theorem ifppos (p a b: wff): $ p -> (ifp p a b <-> a) $ =
'(bitrd (syl bior2 @ con2 anl) bian1);
pub theorem ifpneg (p a b: wff): $ ~p -> (ifp p a b <-> b) $ =
'(bitrd (syl bior1 @ con3 anl) bian1);
theorem ifpid: $ ifp p a a <-> a $ = '(cases ifppos ifpneg);
theorem ifpnot: $ ifp (~p) a b <-> ifp p b a $ =
'(bitr4 orcomb @ oreq1 @ aneq1i notnot);
theorem ifpan1: $ ifp p a b /\ c <-> ifp p (a /\ c) (b /\ c) $ =
'(bitr andir @ oreq anass anass);
theorem ifpan2: $ c /\ ifp p a b <-> ifp p (c /\ a) (c /\ b) $ =
'(bitr andi @ oreq anlass anlass);
theorem ifpor: $ ifp p (a \/ b) (c \/ d) <-> ifp p a c \/ ifp p b d $ =
(let ([(f x) '(bitr4d ,x @ oreqd ,x ,x)]) '(cases ,(f 'ifppos) ,(f 'ifpneg)));
theorem ifpeq1a: $ (p -> (a1 <-> a2)) -> (ifp p a1 b <-> ifp p a2 b) $ = '(oreq1d aneq2a);
theorem ifpeq2a: $ (~p -> (b1 <-> b2)) -> (ifp p a b1 <-> ifp p a b2) $ = '(oreq2d aneq2a);
theorem ifptreq (h: $ G -> (p <-> ifp a p0 p1) $)
(h0: $ G /\ a -> (p0 <-> q0) $) (h1: $ G /\ ~a -> (p1 <-> q1) $):
$ G -> (p <-> ifp a q0 q1) $ =
'(bitrd h @ bitrd (syl ifpeq1a @ exp h0) (syl ifpeq2a @ exp h1));
theorem ifppos2: $ b -> (ifp a b c <-> a \/ c) $ = '(syl6bb (oreq2a bian1) (oreq1d bian2));
theorem ifppos3: $ c -> (ifp a b c <-> ~a \/ b) $ = '(syl5bbr ifpnot ifppos2);
theorem ifpneg3: $ ~c -> (ifp a b c <-> a /\ b) $ = '(syl bior2 @ con3 anr);
theorem ifpneg2: $ ~b -> (ifp a b c <-> ~a /\ c) $ = '(syl5bbr ifpnot ifpneg3);
--| The constant `true`.
@(add-eval #t)
term tru: wff; prefix tru: $T.$ prec max;
--| `true` is true.
axiom itru: $ T. $;
--| The constant `false`.
@(add-eval) def fal: wff = $ ~T. $; prefix fal: $F.$ prec max;
theorem trud (h: $ T. -> a $): $ a $ = '(h itru);
theorem eqtru: $ (a <-> T.) <-> a $ =
'(ibii (mpbiri itru id) @ bithd id (a1i itru));
theorem notfal: $ ~F. $ = '(notnot1 itru);
theorem efal: $ F. -> a $ = '(absurd notfal);
theorem imfal: $ (a -> F.) <-> ~a $ = '(ibii (mpi notfal con3) absurd);
theorem eqfal: $ (a <-> F.) <-> ~a $ = '(bitr (bian2 efal) imfal);
theorem neqfal: $ (~a <-> F.) <-> a $ = '(bitr4 eqfal notnot);
--| The sort of natural numbers, or nonnegative integers.
--| In Peano Arithmetic this is the domain of discourse,
--| the basic sort over which quantifiers range.
sort nat;
--| The for-all quantifier. `A. x p` means
--| "for all natural numbers `x`, `p` holds",
--| where `(p: wff x)` in the declaration indicates that `p` may contain
--| free occurrences of variable `x` that are bound by this quantifier.
term al {x: nat} (p: wff x): wff; prefix al: $A.$ prec 41;
--| The exists quantifier. `E. x p` means
--| "there is a natural number `x`, such that `p` holds",
--| where `(p: wff x)` in the declaration indicates that `p` may contain
--| free occurrences of variable `x` that are bound by this quantifier.
def ex {x: nat} (p: wff x): wff = $ ~(A. x ~p) $;
prefix ex: $E.$ prec 41;
--| Equality of natural numbers: `a = b`
--| means that `a` and `b` have the same value.
@(add-eval @ fn (a b) {(eval a) = (eval b)})
term eq (a b: nat): wff; infixl eq: $=$ prec 50;
--| The axiom of generalization. If `|- p` is derivable
--| (the lack of a precondition means this is a proof in the empty context),
--| then `p` is universally true, so `|- A. x p` is also true.
axiom ax_gen {x: nat} (p: wff x): $ p $ > $ A. x p $;
--| Axiom 4 for predicate logic: forall distributes over implication.
axiom ax_4 {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $;
theorem alim {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $ = 'ax_4;
--| Axiom 5 for predicate logic: If `p` does not contain an occurrence of `x`
--| (note that `(p: wff)` in contrast to `(p: wff x)` means that `p` cannot
--| depend on variable `x`), then `p` implies `A. x p`
--| because the quantifier is trivial.
axiom ax_5 {x: nat} (p: wff): $ p -> A. x p $;
theorem ial {x: nat} (p: wff): $ p -> A. x p $ = 'ax_5;
--| Axiom 6 for predicate logic: for any term `a` (which cannot depend on `x`),
--| there exists an `x` which is equal to `a`.
axiom ax_6 (a: nat) {x: nat}: $ E. x x = a $;
--| Axiom 7 for predicate logic: equality satisfies the euclidean property
--| (which implies symmetry and transitivity, and reflexivity given axiom 6).
axiom ax_7 (a b c: nat): $ a = b -> a = c -> b = c $;
theorem eqtr3: $ b = a -> b = c -> a = c $ = 'ax_7;
-- axiom 9 has been proven redundant; axiom 8 is displaced below
--| Axiom 10 for predicate logic: `x` is bound in `~(A. x p)`, so we can
--| safely introduce a `A. x` quantifier. (This axiom is used to internalize
--| the notion of "bound in" when axiom 5 does not apply.)
axiom ax_10 {x: nat} (p: wff x): $ ~(A. x p) -> A. x ~(A. x p) $;
--| Axiom 11 for predicate logic: forall quantifiers commute.
axiom ax_11 {x y: nat} (p: wff x y): $ A. x A. y p -> A. y A. x p $;
theorem alcom {x y: nat} (p: wff x y): $ A. x A. y p -> A. y A. x p $ = 'ax_11;
--| Axiom 12 for predicate logic: If `x` is some fixed `a` and `p(x)` holds,
--| then for all `x` which are equal to `a`, `p(x)` holds. This expresses the
--| substitution property of `=`, but the name shadowing on `x` allows us to
--| express this without changing `p`,
--| because we haven't defined proper substitution yet.
axiom ax_12 {x: nat} (a: nat) (p: wff x): $ x = a -> p -> A. x (x = a -> p) $;
theorem alimi (a b: wff x) (h: $ a -> b $): $ A. x a -> A. x b $ = '(ax_4 (ax_gen h));
theorem iald (a: wff) (b: wff x) (h: $ a -> b $): $ a -> A. x b $ = '(syl (alimi h) ax_5);
theorem eex (a: wff x) (b: wff) (h: $ a -> b $): $ E. x a -> b $ = '(con1 @ iald @ con3 h);
theorem eqid: $ a = a $ = '(!! eex x (imidm ax_7) ax_6);
theorem eqcom: $ a = b -> b = a $ = '(mpi eqid ax_7);
theorem eqtr: $ a = b -> b = c -> a = c $ = '(syl ax_7 eqcom);
theorem eqtr2: $ a = b -> b = c -> c = a $ = '(syl6 eqcom eqtr);
theorem eqtr4: $ a = b -> c = b -> a = c $ = '(syl5 eqcom eqtr);
theorem eqcomb: $ a = b <-> b = a $ = '(ibii eqcom eqcom);
theorem eqeq1: $ a = b -> (a = c <-> b = c) $ = '(ibid eqtr3 eqtr);
theorem eqeq2: $ b = c -> (a = b <-> a = c) $ = '(ibid (com12 eqtr) (com12 eqtr4));
theorem eqeq1d (h: $ G -> a = b $): $ G -> (a = c <-> b = c) $ = '(syl eqeq1 h);
theorem eqeq2d (h: $ G -> b = c $): $ G -> (a = b <-> a = c) $ = '(syl eqeq2 h);
@(register-eqd 'eq) theorem eqeqd (h1: $ G -> a = b $) (h2: $ G -> c = d $):
$ G -> (a = c <-> b = d) $ = '(bitrd (eqeq1d h1) (eqeq2d h2));
theorem eqeq: $ a = b -> c = d -> (a = c <-> b = d) $ = '(exp (eqeqd anl anr));
theorem eqtr2d (h1: $ G -> a = b $) (h2: $ G -> b = c $): $ G -> c = a $ = '(sylc eqtr2 h1 h2);
theorem eqtr3d (h1: $ G -> b = a $) (h2: $ G -> b = c $): $ G -> a = c $ = '(sylc eqtr3 h1 h2);
theorem eqidd: $ G -> a = a $ = '(a1i eqid);
theorem eqcomi (h: $ a = b $): $ b = a $ = '(eqcom h);
theorem eqcomd (h: $ G -> a = b $): $ G -> b = a $ = '(syl eqcom h);
theorem eqtrd (h1: $ G -> a = b $) (h2: $ G -> b = c $): $ G -> a = c $ = '(sylc eqtr h1 h2);
theorem eqtr4i (h1: $ a = b $) (h2: $ c = b $): $ a = c $ = '(eqtr4 h1 h2);
theorem eqtr4d (h1: $ G -> a = b $) (h2: $ G -> c = b $): $ G -> a = c $ = '(sylc eqtr4 h1 h2);
theorem syl5eq (h1: $ a = b $) (h2: $ G -> b = c $): $ G -> a = c $ = '(eqtrd (a1i h1) h2);
theorem syl5eqr (h1: $ b = a $) (h2: $ G -> b = c $): $ G -> a = c $ = '(eqtr3d (a1i h1) h2);
theorem syl6eq (h1: $ b = c $) (h2: $ G -> a = b $): $ G -> a = c $ = '(eqtrd h2 (a1i h1));
theorem syl6eqr (h1: $ c = b $) (h2: $ G -> a = b $): $ G -> a = c $ = '(eqtr4d h2 (a1i h1));
theorem eqtr3g (h1: $ a = c $) (h2: $ b = d $) (h: $ G -> a = b $):
$ G -> c = d $ = '(syl5eqr h1 @ syl6eq h2 h);
theorem eqtr4g (h1: $ c = a $) (h2: $ d = b $) (h: $ G -> a = b $):
$ G -> c = d $ = '(syl5eq h1 @ syl6eqr h2 h);
theorem aleq (a b: wff x): $ A. x (a <-> b) -> (A. x a <-> A. x b) $ =
'(ibid (syl ax_4 @ alimi bi1) (syl ax_4 @ alimi bi2));
theorem aleqi (a b: wff x) (h: $ a <-> b $): $ A. x a <-> A. x b $ = '(aleq @ ax_gen h);
theorem alimd (G) (a b: wff x) (h: $ G -> a -> b $):
$ G -> A. x a -> A. x b $ = '(syl ax_4 @ syl (alimi h) ax_5);
theorem raleqi (p a b: wff x) (h: $ a <-> b $): $ A. x (p -> a) <-> A. x (p -> b) $ = '(aleqi @ imeq2i h);
theorem al2imi (a b c: wff x) (h: $ a -> b -> c $): $ A. x a -> A. x b -> A. x c $ =
'(syl alim @ alimi h);
@(register-eqd 'al) theorem aleqd (G) {x} (a b: wff x) (h: $ G -> (a <-> b) $):
$ G -> (A. x a <-> A. x b) $ = '(syl aleq @ iald h);
theorem ialda (G: wff) (a b: wff x) (h: $ G /\ a -> b $): $ G -> A. x (a -> b) $ = '(iald @ exp h);
theorem alcomb (a: wff x y): $ A. x A. y a <-> A. y A. x a $ = '(ibii alcom alcom);
theorem alan (a b: wff x): $ A. x (a /\ b) <-> A. x a /\ A. x b $ =
'(ibii (iand (alimi anl) (alimi anr)) (imp @ al2imi ian));
theorem ralan (a b c: wff x): $ A. x (a -> (b /\ c)) <-> A. x (a -> b) /\ A. x (a -> c) $ =
'(bitr (aleqi imandi) alan);
theorem exim (a b: wff x): $ A. x (a -> b) -> E. x a -> E. x b $ = '(syl con3 @ al2imi con3);
theorem eximi (a b: wff x) (h: $ a -> b $): $ E. x a -> E. x b $ = '(exim @ ax_gen h);
theorem exeq (a b: wff x): $ A. x (a <-> b) -> (E. x a <-> E. x b) $ =
'(noteqd @ syl aleq @ alimi noteq);
@(register-eqd 'ex) theorem exeqd (G) {x} (a b: wff x) (h: $ G -> (a <-> b) $):
$ G -> (E. x a <-> E. x b) $ = '(syl exeq @ iald h);
theorem exeqi (a b: wff x) (h: $ a <-> b $): $ E. x a <-> E. x b $ = '(exeq @ ax_gen h);
theorem rexeqi (p a b: wff x) (h: $ a <-> b $): $ E. x (p /\ a) <-> E. x (p /\ b) $ = '(exeqi @ aneq2i h);
theorem rexeqa (p a b: wff x) (h: $ p -> (a <-> b) $): $ E. x (p /\ a) <-> E. x (p /\ b) $ = '(exeqi @ aneq2a h);
theorem rexeqd (p a b: wff x) (h: $ G -> (a <-> b) $): $ G -> (E. x (p /\ a) <-> E. x (p /\ b)) $ = '(exeqd @ aneq2d h);
theorem rexeqda (p a b: wff x) (h: $ G /\ p -> (a <-> b) $): $ G -> (E. x (p /\ a) <-> E. x (p /\ b)) $ = '(exeqd @ aneq2da h);
theorem iex (a: wff x): $ a -> E. x a $ =
'(!! eex y (rsyl eqcom @ syl6 (mpi ax_6 exim) ax_12) ax_6);
theorem alanex (a b: wff x): $ A. x a /\ E. x b -> E. x (a /\ b) $ = '(imp @ syl exim @ alimi ian);
theorem exanal (a b: wff x): $ E. x a /\ A. x b -> E. x (a /\ b) $ = '(impcom @ syl exim @ alimi @ com12 ian);
theorem alnex (a: wff x): $ A. x ~a <-> ~(E. x a) $ = 'notnot;
theorem ngen (a: wff x) (h: $ ~a $): $ ~E. x a $ = '(notnot1 (ax_gen h));
theorem alex (a: wff x): $ A. x a <-> ~(E. x ~a) $ =
'(bitr (aleqi notnot) alnex);
theorem exnal (a: wff x): $ E. x ~a <-> ~(A. x a) $ = '(con2b alex);
theorem eal (a: wff x): $ A. x a -> a $ = '(ax_3 @ sylib exnal iex);
theorem albi: $ A. x a <-> a $ = '(ibii eal ial);
theorem exbi: $ E. x a <-> a $ = '(con1b @ bicom albi);
theorem alan1 (b: wff x): $ A. x (a /\ b) <-> a /\ A. x b $ = '(bitr alan @ aneq1i albi);
theorem alan2 (a: wff x): $ A. x (a /\ b) <-> A. x a /\ b $ = '(bitr alan @ aneq2i albi);
theorem exor (a b: wff x): $ E. x (a \/ b) <-> E. x a \/ E. x b $ =
'(bitr (noteqi (bitr (aleqi notor) alan)) notan);
theorem eximd (G) (a b: wff x) (h: $ G -> a -> b $): $ G -> E. x a -> E. x b $ = '(syl exim @ iald h);
theorem excomb (a: wff x y): $ E. x E. y a <-> E. y E. x a $ =
'(noteq @ bitr3 (aleqi alnex) @ bitr alcomb (aleqi alnex));
theorem excom (a: wff x y): $ E. x E. y a -> E. y E. x a $ = '(bi1 excomb);
theorem nexi (a: wff x) (h: $ ~a $): $ ~E. x a $ = '(mpbi alnex @ ax_gen h);
theorem nexd (a: wff x) (h: $ G -> ~a $): $ G -> ~E. x a $ = '(sylib alnex @ iald h);
theorem exim1 (a: wff) (b: wff x): $ E. x (a -> b) -> (a -> E. x b) $ = '(com12 @ eximd mpcom);
@_ local def nf {x: nat} (a: wff x): wff = $ A. x (a -> A. x a) $;
prefix nf: $F/$ prec 10;
theorem nfv: $ F/ x a $ = '(ax_gen ax_5);
theorem nfi (a: wff x) (h: $ F/ x a $): $ a -> A. x a $ = '(eal h);
theorem nfri (a: wff x) (h: $ a -> A. x a $): $ F/ x a $ = '(ax_gen h);
theorem nfeqi (a b: wff x) (h: $ a <-> b $): $ (F/ x a) <-> (F/ x b) $ = '(trud @ nfeqd @ a1i h);
theorem nfx (a b: wff x) (h1: $ a <-> b $) (h2: $ F/ x b $): $ F/ x a $ = '(bi2i (nfeqi h1) h2);
theorem nfal (a: wff x y) (h: $ F/ x a $): $ F/ x A. y a $ =
'(nfri @ syl ax_11 @ alimi @ nfi h);
theorem nfnot (a: wff x) (h: $ F/ x a $): $ F/ x ~a $ =
'(nfri @ con1 @ syl eal @ syl (con1 @ !! ax_10 x) @ eximi @ nfi h);
theorem nfim (a b: wff x) (h1: $ F/ x a $) (h2: $ F/ x b $): $ F/ x a -> b $ =
'(nfri @ cases
(syl6 (syl (alimi ax_1) (nfi h2)) mpcom)
(a1d @ syl (alimi absurd) @ nfi @ nfnot h1));
theorem nfan (a b: wff x) (h1: $ F/ x a $) (h2: $ F/ x b $): $ F/ x a /\ b $ = '(nfnot @ nfim h1 @ nfnot h2);
theorem nfor (a b: wff x) (h1: $ F/ x a $) (h2: $ F/ x b $): $ F/ x a \/ b $ = '(nfim (nfnot h1) h2);
theorem nfbi (a b: wff x) (h1: $ F/ x a $) (h2: $ F/ x b $): $ F/ x a <-> b $ = '(nfan (nfim h1 h2) (nfim h2 h1));
theorem nfex1 (a: wff x): $ F/ x E. x a $ = '(ax_gen ax_10);
theorem nfex (a: wff x y) (h: $ F/ x a $): $ F/ x E. y a $ = '(nfnot @ nfal @ nfnot h);
theorem nfal1 (a: wff x): $ F/ x A. x a $ = '(nfx alex @ nfnot nfex1);
theorem ialdh (a b: wff x) (h1: $ F/ x a $) (h2: $ a -> b $): $ a -> A. x b $ =
'(syl (alimi h2) (nfi h1));
theorem eexh (a b: wff x) (h1: $ F/ x b $) (h2: $ a -> b $): $ E. x a -> b $ =
'(con1 @ ialdh (nfnot h1) @ con3 h2);
theorem eexdh (a b c: wff x) (h1: $ F/ x a $) (h2: $ F/ x c $)
(h3: $ a -> b -> c $): $ a -> E. x b -> c $ =
'(con1d @ exp @ ialdh (nfan h1 (nfnot h2)) (imp @ con3d h3));
theorem alimdh (a b c: wff x) (h1: $ F/ x a $) (h2: $ a -> b -> c $):
$ a -> A. x b -> A. x c $ = '(syl alim @ ialdh h1 h2);
theorem aleqdh (G a b: wff x) (h1: $ F/ x G $) (h: $ G -> (a <-> b) $):
$ G -> (A. x a <-> A. x b) $ = '(syl aleq @ ialdh h1 h);
theorem eexd (a: wff) (b: wff x) (c: wff)
(h: $ a -> b -> c $): $ a -> E. x b -> c $ = '(eexdh nfv nfv h);
theorem eexda (a: wff) (b: wff x) (c: wff)
(h: $ a /\ b -> c $): $ a -> E. x b -> c $ = '(eexd (exp h));
theorem eexb (a: wff x) (b: wff): $ (E. x a -> b) <-> A. x (a -> b) $ =
'(ibii (ialdh (nfim nfex1 nfv) (imim1i iex)) (eexdh nfal1 nfv eal));
theorem erexb (a b: wff x) (c: wff): $ (E. x (a /\ b) -> c) <-> A. x (a -> b -> c) $ =
'(bitr eexb @ aleqi impexp);
theorem iexeh (a: nat) (b c: wff x) (h: $ F/ x c $)
(e: $ x = a -> (b <-> c) $): $ c -> E. x b $ =
'(mpi ax_6 @ syl exim @ ialdh h @ com12 @ bi2d e);
theorem ealeh (a: nat) (b c: wff x) (h: $ F/ x c $)
(e: $ x = a -> (b <-> c) $): $ A. x b -> c $ =
'(ax_3 @ sylib exnal @ iexeh (nfnot h) @ noteqd e);
theorem alim1 (a) (b: wff x): $ A. x (a -> b) <-> a -> A. x b $ =
'(ibii (com12 @ alimd mpcom) (ialdh (nfim nfv nfal1) @ imim2i eal));
theorem ralim1 (a) (p b: wff x): $ A. x (p -> a -> b) <-> a -> A. x (p -> b) $ =
'(bitr (aleqi com12b) alim1);
theorem ralalcomb (p: wff x) (a: wff x y): $ A. x (p -> A. y a) <-> A. y A. x (p -> a) $ =
'(bitr3 (aleqi alim1) alcomb);
theorem ralcomb (p: wff x) (q: wff y) (a: wff x y):
$ A. x (p -> A. y (q -> a)) <-> A. y (q -> A. x (p -> a)) $ =
'(bitr ralalcomb @ aleqi ralim1);
theorem exal (a: wff x y): $ E. x A. y a -> A. y E. x a $ = '(eexh (nfal nfex1) @ alimi iex);
theorem exral (a: wff y) (b: wff x y):
$ E. x A. y (a -> b) -> A. y (a -> E. x b) $ = '(rsyl exal @ alimi exim1);
theorem rexal (a: wff x) (b: wff x y):
$ E. x (a /\ A. y b) -> A. y E. x (a /\ b) $ = '(sylbir (exeqi alan1) @ exal);
theorem rexim1 (a c: wff x): $ E. x (a /\ (b -> c)) -> (b -> E. x (a /\ c)) $ =
'(com12 @ eximd @ anim2d mpcom);
theorem rexral (a: wff x) (b: wff y) (c: wff x y):
$ E. x (a /\ A. y (b -> c)) -> A. y (b -> E. x (a /\ c)) $ =
'(syl exral @ eximi @ sylbir alan1 @ alimi imancom);