-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathstdlib.bus
More file actions
7954 lines (5950 loc) · 225 KB
/
stdlib.bus
File metadata and controls
7954 lines (5950 loc) · 225 KB
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
/*
Language built-ins:
atom IMPLIES;
syntax (a b) = a b, precedence 10000, associativity left;
*/
syntax (a -> b) = IMPLIES a b, precedence 100, associativity right;
assume todo proves forany a: a;
define FALSE = forany a: a;
syntax (!a) = a -> FALSE, precedence 20000, associativity right;
require false_proves_anything proves forany a: FALSE -> a by ( assume f proves FALSE; unwrap f );
assume not_not_impl proves forany a: ((a -> FALSE) -> FALSE) -> a;
atom AND;
syntax (a && b) = AND a b, precedence 150, associativity left;
assume and_left proves forany a,b: (a && b) -> a;
assume and_right proves forany a,b: (a && b) -> b;
assume impl_impl_and proves forany a,b: a -> b -> (a && b);
define eq x y = (x -> y) && (y -> x);
syntax (a == b) = eq a b, precedence 160, associativity noassoc;
syntax (a != b) = !(a == b), precedence 160, associativity noassoc;
assume func_eq proves forany f,g: (f == g) == (forany x,y: x == y -> f x == g y);
define or a b = !(!a && !b);
syntax (a || b) = or a b, precedence 150, associativity left;
define xor a b = (a || b) && !(a && b);
syntax (a ^^ b) = xor a b, precedence 150, associativity left;
atom HAS_MEMBER;
syntax (a : b) = HAS_MEMBER b a, precedence 200, associativity noassoc;
atom SWITCH;
assume switch_yes proves forany arg,cond,eqval,neqval: (arg == cond) -> (SWITCH arg cond eqval neqval == eqval );
assume switch_no proves forany arg,cond,eqval,neqval: (arg != cond) -> (SWITCH arg cond eqval neqval == neqval);
atom UINT;
atom UINT_ZERO;
atom UINT_SUCC;
syntax (a++) = UINT_SUCC a, precedence 20000, associativity left;
assume zero_is_uint proves HAS_MEMBER UINT UINT_ZERO;
assume succ_uint_is_uint proves forany a: (a : UINT) -> HAS_MEMBER UINT (UINT_SUCC a);
assume succ_not_zero proves forany a: eq (UINT_SUCC a) UINT_ZERO -> FALSE;
assume uint_is_zero_or_succ proves forany a: a : UINT -> or (eq a UINT_ZERO) ((forany b: (HAS_MEMBER UINT b -> (eq a (UINT_SUCC b)) -> FALSE)) -> FALSE);
assume uint_inductive proves forany a,P: P UINT_ZERO -> (forany b: (b : UINT) -> P b -> P (UINT_SUCC b)) -> (a : UINT) -> P a;
scope (
atom UINT_ZERO;
atom UINT_SUCC;
define IS_UINT n = (n == UINT_ZERO) || !(forany x: !(UINT_SUCC x == n));
);
define UINT_ONE = UINT_SUCC UINT_ZERO;
define UINT_TWO = UINT_SUCC UINT_ONE;
atom UINT_PRED;
assume uint_pred proves forany a: (a : UINT) -> eq (UINT_PRED (UINT_SUCC a)) a;
//define UINT_PRED a = SWITCH a UINT_ZERO UNDEFINED (UINT_SATPRED a);
define UINT_ADD a b = SWITCH b UINT_ZERO a (UINT_SUCC (UINT_ADD a (UINT_PRED b)));
syntax (a + b) = UINT_ADD a b, precedence 200, associativity left;
define UINT_MUL a b = SWITCH b UINT_ZERO UINT_ZERO (UINT_ADD (UINT_MUL a (UINT_PRED b)) a);
syntax (a * b) = UINT_MUL a b, precedence 210, associativity left;
define UINT_POW a b = SWITCH b UINT_ZERO UINT_ONE (UINT_MUL (UINT_POW a (UINT_PRED b)) a);
syntax (a ** b) = UINT_POW a b, precedence 220, associativity right;
define uint_le a b = (forany c: ((c : UINT) && (b == (a + c))) -> FALSE) -> FALSE;
syntax (a <= b) = uint_le a b, precedence 190, associativity noassoc;
define UINT_SATPRED a = SWITCH a UINT_ZERO UINT_ZERO (UINT_PRED a);
define UINT_SATSUB a b = SWITCH a UINT_ZERO UINT_ZERO (SWITCH b UINT_ZERO a (UINT_SATSUB (UINT_PRED a) (UINT_PRED b)));
syntax (a - b) = UINT_SATSUB a b, precedence 200, associativity left;
// define UINT_SATSUB a b = SWITCH b UINT_ZERO a (UINT_SATSUB (UINT_SATPRED a) (UINT_SATPRED b))
// TODO:
assume satsub_succ__satpred_satsub proves forany a,b: a : UINT -> b : UINT -> (a - b++) == UINT_SATPRED (a - b);
define is_divisible_by n o = (n : UINT) && (o : UINT) && !(forany x: !((x : UINT) && x * o == n));
define is_even n = is_divisible_by n UINT_TWO;
define is_prime p = forany d: (p : UINT) && p != UINT_ONE && (d : UINT -> d != UINT_ONE -> d != p -> !(is_divisible_by p d));
define MUL_RANGE first last = SWITCH first last first (first * MUL_RANGE first++ last);
require impl_same proves forany a: a -> a
by (
forany a:
assume A proves a;
A
);
require impl_reverse proves forany a,b: (a -> b) -> (!b -> !a)
by (
forany a,b:
assume AB proves a -> b;
assume BF proves b -> FALSE; // !b
assume A proves a;
(A > AB) > BF
);
require impl_not_not proves forany a: a -> !!a
by (
forany a:
assume A proves a;
assume NA proves (a -> FALSE);
A > NA
);
require not_not_eq proves forany a: ((a -> FALSE) -> FALSE) == a
by (
wrap eq (impl_impl_and < not_not_impl < impl_not_not)
);
require left_impl_not_right__not_and proves forany a,b: (a -> !b) -> !(a && b)
by (
forany a,b:
assume a_nb proves a -> !b;
assume a_and_b proves a && b;
a_nb < (a_and_b > and_left) < (a_and_b > and_right)
);
require right_impl_not_left__not_and proves forany a,b: (b -> !a) -> !(a && b)
by (
forany a,b:
assume b_na proves b -> !a;
assume a_and_b proves a && b;
b_na < (a_and_b > and_right) < (a_and_b > and_left)
);
require yay_or_nay proves forany a: a || !a
by (
forany aa:
require temp proves !(!aa && !!aa)
by (substitute a=!aa in impl_not_not) > left_impl_not_right__not_and;
wrap or temp
);
require or__not_left__right proves forany a,b: a || b -> !a -> b
by (
forany a,b:
assume A_OR_B proves a || b;
assume NA proves !a;
require A_OR_B_ proves !(!a && !b)
by unwrap A_OR_B;
not_not_impl < (
// Goal:
// !!b
assume NB proves !b;
A_OR_B_ < (NB > NA > impl_impl_and)
)
);
require or__not_right__left proves forany a,b: a || b -> !b -> a
by (
forany a,b:
assume A_OR_B proves a || b;
assume NB proves !b;
require A_OR_B_ proves !(!a && !b)
by unwrap A_OR_B;
not_not_impl < (
// Goal:
// !!a
assume NA proves !a;
A_OR_B_ < (NB > NA > impl_impl_and)
)
);
require impl_weaken proves forany a,b: a -> (b -> a)
by (
forany a,b:
assume A proves a;
assume _ proves b;
A
);
require impl_trans proves forany a,b,c: (a -> b) -> (b -> c) -> (a -> c)
by (
forany a,b,c:
assume AB proves a -> b;
assume BC proves b -> c;
assume A proves a;
(A > AB) > BC
);
require impl_impl_impl__and_impl proves forany a,b,c: (a -> b -> c) -> (a && b -> c)
by (
forany a,b,c:
assume abc proves a -> b -> c;
assume ab proves a && b;
(ab > and_right) > (ab > and_left) > abc
);
require impl_reverse_back proves forany a,b: (!b -> !a) -> (a -> b)
by (
forany a,b:
assume NB_NA proves !b -> !a;
assume A proves a;
((A > impl_not_not) > (NB_NA > impl_reverse)) > not_not_impl
);
require or_cases proves forany a,b,c: a || b -> (a -> c) -> (b -> c) -> c
by (
forany a,b,c:
assume ab proves a || b;
assume a_c proves a -> c;
assume b_c proves b -> c;
require nc_na proves !c -> !a by a_c > impl_reverse;
require nc_nb proves !c -> !b by b_c > impl_reverse;
not_not_impl < (
// Goal:
// !!c
assume nc proves !c;
// Goal:
// FALSE
(unwrap ab) < (
// Goal:
// !a && !b
impl_impl_and < (nc > nc_na) < (nc > nc_nb)
)
)
);
require by_contradiction proves forany a: (a -> !a) -> !a
by (
forany a:
assume A_NA proves a -> !a;
assume A proves a;
A > (A > A_NA)
);
require by_contradiction_2 proves forany a: (!a -> a) -> a
by (
forany a:
assume NA_A proves !a -> a;
NA_A > impl_same > yay_or_nay > or_cases
);
require eq_same proves forany a: a == a
by (
wrap eq (impl_same > impl_same > impl_impl_and)
);
require wrap_in_func_impl proves forany f,a,b: a == b -> (f a) == (f b)
by (
forany f,a,b:
assume AB proves eq a b;
AB > eq_same > ((unwrap func_eq) > and_left)
);
require lhs_rhs_eq proves forany f,g,a,b: f == g -> a == b -> (f a) == (g b)
by (
(unwrap func_eq) > and_left
);
require bin_sub_left_impl proves forany f,a,b,x: a == b -> f a x -> f b x
by (
forany f,a,b,x:
assume AB proves eq a b;
assume FAX proves f a x;
require FA_FB proves eq (f a) (f b) by AB > eq_same > lhs_rhs_eq;
FAX > ((unwrap (eq_same > FA_FB > lhs_rhs_eq)) > and_left)
);
require bin_sub_left_eq proves forany f,a,b,x: a == b -> (f a x) == (f b x)
by (
forany f,a,b,x:
assume AB proves eq a b;
eq_same > (AB > (substitute f=f in wrap_in_func_impl)) > lhs_rhs_eq
);
require bin_sub_right_impl proves forany f,a,b,x: a == b -> f x a -> f x b
by (
forany f,a,b,x:
assume AB proves eq a b;
assume FXA proves f x a;
FXA > (unwrap (AB > eq_same > lhs_rhs_eq) > and_left)
);
require bin_sub_right_eq proves forany f,a,b,x: a == b -> (f x a) == (f x b)
by (
forany f,x,a,b:
assume AB proves eq a b;
AB > (substitute a=(f x) in eq_same) > lhs_rhs_eq
);
require un_sub_arg proves forany f,a,b: a == b -> (f a) == (f b)
by wrap_in_func_impl;
require wrap_in_bin_func_lhs proves forany f,a,b,c: a == b -> (f a c) == (f b c)
by (
forany f,a,b,c:
assume ab proves eq a b;
(substitute a=(f a c) in eq_same) > (ab > bin_sub_left_eq) > bin_sub_right_impl
);
require wrap_in_bin_func_rhs proves forany f,a,b,c: a == b -> (f c a) == (f c b)
by (
forany f,a,b,c:
assume ab proves eq a b;
(substitute a=(f c a) in eq_same) > (ab > bin_sub_right_eq) > bin_sub_right_impl
);
require and_comm_impl proves forany a,b: a && b -> b && a
by (
forany a,b:
assume AB proves AND a b;
(AB > and_left) > ((AB > and_right) > impl_impl_and)
);
require and_comm_eq proves forany a,b: (a && b) == (b && a)
by wrap eq ( impl_impl_and < and_comm_impl < and_comm_impl );
require not_left__not_and proves forany a,b: !a -> !(a && b)
by (
forany a,b:
assume NA proves a -> FALSE;
assume AB proves AND a b;
(AB > and_left) > NA
);
require not_right__not_and proves forany a,b: !b -> !(a && b)
by (
forany a,b:
assume NB proves b -> FALSE;
assume AB proves AND a b;
(AB > and_right) > NB
);
require and_same proves forany a: (a && a) == a
by (
forany a:
require ltr proves (AND a a) -> a by and_left;
require rtl proves a -> (AND a a) by (
assume A proves a;
A > A > impl_impl_and
);
wrap eq (rtl > ltr > impl_impl_and)
);
require not_and__left_impl_not_right proves forany a,b: !(a && b) -> a -> !b
by (
forany a,b:
assume not_ab proves !(a && b);
assume A proves a;
assume B proves b;
not_ab < (impl_impl_and < A < B)
);
require not_and__right_impl_not_left proves forany a,b: !(a && b) -> b -> !a
by (
forany a,b:
assume not_ab proves !(a && b);
assume B proves b;
assume A proves a;
not_ab < (impl_impl_and < A < B)
);
require eq_ltr proves forany a,b: a == b -> (a -> b)
by (
forany a,b:
assume AeqB proves a == b;
(unwrap AeqB) > and_left
);
require eq_rtl proves forany a,b: a == b -> (b -> a)
by (
forany a,b:
assume AeqB proves a == b;
(unwrap AeqB) > and_right
);
require eq_comm proves forany a,b: a == b -> b == a
by (
forany a,b:
assume A_eq_B proves a == b;
wrap eq ((unwrap A_eq_B) > and_comm_impl)
);
require eq_comm_eq proves forany a,b: (a == b) == (b == a)
by (
forany a,b:
wrap eq (impl_impl_and < eq_comm < eq_comm)
);
require eq_trans proves forany a,b,c: a == b -> b == c -> a == c
by (
forany a,b,c:
assume A_eq_B proves eq a b;
assume B_eq_C proves eq b c;
A_eq_B > B_eq_C > bin_sub_right_impl
);
require neq_comm proves forany a,b: a != b -> b != a
by (
forany a,b:
assume ab proves a != b;
assume ba proves b == a;
ab < (ba > eq_comm)
);
require neq_same proves forany a: !(a != a)
by eq_same > impl_not_not;
require not_impl__or proves forany a,b: (!a -> b) -> a || b
by (
forany a,b:
assume NA_B proves !a -> b;
wrap or (
assume NA_AND_NB proves !a && !b;
(NA_AND_NB > and_left) > ((NA_AND_NB > and_right) > (NA_B > impl_reverse))
)
);
require or_left proves forany a,b: a -> a || b
by (
forany a,b:
assume A proves a;
wrap or (
assume NA_and_NB proves !a && !b;
A > (NA_and_NB > and_left)
)
);
require or_right proves forany a,b: b -> a || b
by (
forany a,b:
assume B proves b;
wrap or (
assume NA_and_NB proves !a && !b;
B > (NA_and_NB > and_right)
)
);
require or_impl_left proves forany a,b,c: ((a || b) -> c) -> (a -> c)
by (
forany a,b,c:
assume OR_AB_C proves (a || b) -> c;
assume A proves a;
((A > or_left) > OR_AB_C)
);
require or_impl_right proves forany a,b,c: ((a || b) -> c) -> (b -> c)
by (
forany a,b,c:
assume OR_AB_C proves (a || b) -> c;
assume B proves b;
((B > or_right) > OR_AB_C)
);
require or_comm_impl proves forany a,b: a || b -> b || a
by (
forany a,b:
assume A_OR_B proves a || b;
require A_IMPL_B_OR_A proves a -> b || a by or_right;
require B_IMPL_B_OR_A proves b -> b || a by or_left;
B_IMPL_B_OR_A > A_IMPL_B_OR_A > A_OR_B > or_cases
);
require or_comm_eq proves forany a,b: eq (or a b) (or b a)
by wrap eq ( impl_impl_and < or_comm_impl < or_comm_impl );
require false_false__not_or proves forany a,b: !a -> !b -> !(a || b)
by (
forany a,b:
assume NA proves !a;
assume NB proves !b;
assume OR_AB proves or a b;
require OR_AB_ proves (AND !a !b) -> FALSE
by unwrap OR_AB;
(NB > NA > impl_impl_and) > OR_AB_
);
require or_assoc_impl proves forany a,b,c: (a || b) || c -> a || (b || c)
by (
forany a,b,c:
assume AB_C proves (a || b) || c;
require AB_C_ proves AND (or a b -> FALSE) (c -> FALSE) -> FALSE
by unwrap AB_C;
wrap or (
// Goal:
// AND (a -> FALSE) (or b c -> FALSE) -> FALSE
assume NA_NBC proves AND (a -> FALSE) (or b c -> FALSE);
// Goal:
// FALSE
require NA proves a -> FALSE by NA_NBC > and_left;
require NBC proves or b c -> FALSE
by NA_NBC > and_right;
require NBC_ proves (AND (b -> FALSE) (c -> FALSE) -> FALSE) -> FALSE
by (
assume temp proves AND (b -> FALSE) (c -> FALSE) -> FALSE;
(wrap or temp) > NBC
);
require NBC__ proves AND (b -> FALSE) (c -> FALSE)
by NBC_ > not_not_impl;
require NB proves b -> FALSE by NBC__ > and_left;
require NC proves c -> FALSE by NBC__ > and_right;
AB_C_ < (
// Goal:
// AND (or a b -> FALSE) (c -> FALSE)
impl_impl_and < (
// Goal:
// or a b -> FALSE
assume AB proves or a b;
// Goal:
// FALSE
require AB_ proves AND (a -> FALSE) (b -> FALSE) -> FALSE
by unwrap AB;
AB_ < (
impl_impl_and < NA < NB
)
) < NC
)
)
);
require not_not_or_not__and proves forany a,b: (or (a -> FALSE) (b -> FALSE) -> FALSE) -> AND a b
by (
forany a,b:
assume not_na_or_nb proves or (a -> FALSE) (b -> FALSE) -> FALSE;
require temp1 proves (AND ((a -> FALSE) -> FALSE) ((b -> FALSE) -> FALSE) -> FALSE) -> FALSE
by (
assume ttt proves AND ((a -> FALSE) -> FALSE) ((b -> FALSE) -> FALSE) -> FALSE;
wrap or ttt > not_na_or_nb
);
require temp2 proves AND ((a -> FALSE) -> FALSE) ((b -> FALSE) -> FALSE)
by temp1 > not_not_impl;
(temp2 > not_not_eq > bin_sub_left_impl) > not_not_eq > bin_sub_right_impl
);
require xor__not_right__left proves forany a,b: a ^^ b -> !b -> a
by (
forany a,b:
assume XAB proves a ^^ b;
assume NB proves !b;
NB > (((unwrap XAB) > and_left) > or__not_right__left)
);
require xor__not_left__right proves forany a,b: a ^^b -> !a -> b
by (
forany a,b:
assume XAB proves a ^^ b;
assume NA proves !a;
NA > (((unwrap XAB) > and_left) > or__not_left__right)
);
require xor_comm_impl proves forany a,b: a ^^ b -> b ^^ a
by (
forany a,b:
assume XAB proves a ^^ b;
require OR_BA proves b || a by ((unwrap XAB) > and_left) > or_comm_impl;
require NOT_AND_BA proves !(b && a) by ((unwrap XAB) > and_right) > (and_comm_impl > impl_trans);
wrap xor (NOT_AND_BA > OR_BA > impl_impl_and)
);
require xor__left__not_right proves forany a,b: a ^^ b -> a -> !b
by (
forany a,b:
assume XAB proves a ^^ b;
assume A proves a;
assume B proves b;
(B > A > impl_impl_and) > (unwrap XAB > and_right)
);
require xor__right__not_left proves forany a,b: a ^^ b -> b -> !a
by (
forany a,b:
assume XAB proves a ^^ b;
assume B proves b;
assume A proves a;
(B > A > impl_impl_and) > (unwrap XAB > and_right)
);
require true__false__xor proves forany a,b: a -> !b -> a ^^ b
by (
forany a,b:
assume A proves a;
assume NB proves b -> FALSE;
wrap xor (impl_impl_and < (or_left < A) < (not_right__not_and < NB))
);
require false__true__xor proves forany a,b: !a -> b -> a ^^ b
by (
forany a,b:
assume NA proves !a;
assume B proves b;
wrap xor (impl_impl_and < (or_right < B) < (not_left__not_and < NA))
);
require false_false__not_xor proves forany a,b: !a -> !b -> !(a ^^ b)
by (
forany a,b:
assume NA proves !a;
assume NB proves !b;
assume XAB proves a ^^ b;
(unwrap XAB) > (NB > NA > false_false__not_or) > not_left__not_and
);
require UINT_SATSUB_switcheq proves forany a,b: UINT_SATSUB a b == SWITCH a UINT_ZERO UINT_ZERO (SWITCH b UINT_ZERO a (UINT_SATSUB (UINT_PRED a) (UINT_PRED b)))
by (
forany a,b:
wrap eq (
impl_impl_and
< ( assume a1 proves UINT_SATSUB a b; unwrap a1 )
< ( assume a2 proves SWITCH a UINT_ZERO UINT_ZERO (SWITCH b UINT_ZERO a (UINT_SATSUB (UINT_PRED a) (UINT_PRED b))); wrap UINT_SATSUB a2 )
)
);
require zero_satsub proves forany a: a : UINT -> UINT_ZERO - a == UINT_ZERO
by (
forany a:
assume auint proves a : UINT;
require temp1 proves (UINT_ZERO - a) == (UINT_ZERO - a) by eq_same;
require temp2 proves (UINT_ZERO - a) == SWITCH UINT_ZERO UINT_ZERO UINT_ZERO (SWITCH a UINT_ZERO UINT_ZERO (UINT_SATSUB (UINT_PRED UINT_ZERO) (UINT_PRED a)))
by temp1 > UINT_SATSUB_switcheq > bin_sub_right_impl;
require temp3 proves (UINT_ZERO - a) == UINT_ZERO
by temp2 > (switch_yes < eq_same) > bin_sub_right_impl;
temp3
);
require satsub_zero proves forany a: a : UINT -> UINT_SATSUB a UINT_ZERO == a
by (
forany a:
assume auint proves a : UINT;
or_cases < (uint_is_zero_or_succ < auint) < (
assume a_0 proves a == UINT_ZERO;
((zero_satsub < zero_is_uint) > (a_0 > eq_comm) > bin_sub_right_impl) > ((a_0 > eq_comm) > bin_sub_left_eq) > bin_sub_left_impl
) < (
assume a_succ proves (forany c: (HAS_MEMBER UINT c -> (eq a (UINT_SUCC c)) -> FALSE)) -> FALSE;
not_not_impl < (
assume ttt proves (UINT_SATSUB a UINT_ZERO == a) -> FALSE;
a_succ < (
forany c:
assume cuint proves c : UINT;
assume a_sc proves a == c++;
require a_not_0 proves a != UINT_ZERO
by (substitute a=c in succ_not_zero) > ((a_sc > eq_comm) > bin_sub_left_eq) > bin_sub_left_impl;
ttt < (
// Goal:
// a - UINT_ZERO == a
require temp1 proves a - UINT_ZERO == a - UINT_ZERO by eq_same;
require temp2 proves a - UINT_ZERO == SWITCH a UINT_ZERO UINT_ZERO (SWITCH UINT_ZERO UINT_ZERO a (UINT_SATSUB (UINT_PRED a) (UINT_PRED UINT_ZERO)))
by temp1 > UINT_SATSUB_switcheq > bin_sub_right_impl;
require temp3 proves a - UINT_ZERO == (SWITCH UINT_ZERO UINT_ZERO a (UINT_SATSUB (UINT_PRED a) (UINT_PRED UINT_ZERO)))
by temp2 > (switch_no < a_not_0) > bin_sub_right_impl;
require temp4 proves a - UINT_ZERO == a
by temp3 > (switch_yes < eq_same) > bin_sub_right_impl;
temp4
)
)
)
)
);
require succ_satsub_succ proves forany a, b: a : UINT -> b : UINT -> UINT_SATSUB a++ b++ == UINT_SATSUB a b
by (
forany a,b:
assume auint proves a : UINT;
assume buint proves b : UINT;
require temp1 proves UINT_SATSUB a++ b++ == UINT_SATSUB a++ b++ by eq_same;
require temp2 proves UINT_SATSUB a++ b++ == SWITCH a++ UINT_ZERO UINT_ZERO (SWITCH b++ UINT_ZERO a++ (UINT_SATSUB (UINT_PRED a++) (UINT_PRED b++)))
by temp1 > UINT_SATSUB_switcheq > bin_sub_right_impl;
require temp3 proves UINT_SATSUB a++ b++ == SWITCH b++ UINT_ZERO a++ (UINT_SATSUB (UINT_PRED a++) (UINT_PRED b++))
by temp2 > (switch_no < succ_not_zero) > bin_sub_right_impl;
require temp4 proves UINT_SATSUB a++ b++ == UINT_SATSUB (UINT_PRED a++) (UINT_PRED b++)
by temp3 > (switch_no < succ_not_zero) > bin_sub_right_impl;
(temp4 > ((uint_pred < auint) > bin_sub_left_eq) > bin_sub_right_impl)
> ((uint_pred < buint) > bin_sub_right_eq) > bin_sub_right_impl
);
require UINT_SATPRED_switcheq proves forany a: UINT_SATPRED a == SWITCH a UINT_ZERO UINT_ZERO (UINT_PRED a)
by (
forany a:
wrap eq (
impl_impl_and
< ( assume a1 proves UINT_SATPRED a; unwrap a1 )
< ( assume a2 proves SWITCH a UINT_ZERO UINT_ZERO (UINT_PRED a); wrap UINT_SATPRED a2 )
)
);
require sat_pred_zero_is_zero proves UINT_SATPRED UINT_ZERO == UINT_ZERO
by (
require temp1 proves SWITCH UINT_ZERO UINT_ZERO UINT_ZERO (UINT_PRED UINT_ZERO) == SWITCH UINT_ZERO UINT_ZERO UINT_ZERO (UINT_PRED UINT_ZERO)
by eq_same;
(temp1 > (UINT_SATPRED_switcheq > eq_comm) > bin_sub_left_impl) > (eq_same > switch_yes) > bin_sub_right_impl
);
require sat_pred_succ proves forany a: a : UINT -> UINT_SATPRED (a++) == a
by (
forany a:
assume auint proves a : UINT;
(((substitute a=a in succ_not_zero) > switch_no) > (UINT_SATPRED_switcheq > eq_comm) > bin_sub_left_impl) > (auint > uint_pred) > bin_sub_right_impl
);
require sat_pred__succ_satsub proves forany a,b: a : UINT -> b : UINT -> UINT_SATPRED (a++ - b) == a - b
by (
forany a,b:
assume auint proves a : UINT;
assume buint proves b : UINT;
or_cases < (uint_is_zero_or_succ < buint) < (
assume b_0 proves b == UINT_ZERO;
require temp1 proves UINT_SATPRED (a++) == UINT_SATPRED (a++)
by eq_same;
require temp2 proves UINT_SATPRED (a++) == a
by temp1 > (sat_pred_succ < auint) > bin_sub_right_impl;
require temp3 proves UINT_SATPRED (a++) == a - UINT_ZERO
by temp2 > ((satsub_zero < auint) > eq_comm) > bin_sub_right_impl;
require temp4 proves UINT_SATPRED (a++ - UINT_ZERO) == a - UINT_ZERO
by temp3 > (((satsub_zero < (succ_uint_is_uint < auint)) > eq_comm) > un_sub_arg) > bin_sub_left_impl;
require temp5 proves UINT_SATPRED (a++ - UINT_ZERO) == a - b
by temp4 > ((b_0 > eq_comm) > bin_sub_right_eq) > bin_sub_right_impl;
temp5 > (un_sub_arg < (bin_sub_right_eq < (b_0 > eq_comm))) > bin_sub_left_impl
) < (
assume b_succ proves (forany c: (HAS_MEMBER UINT c -> (eq b (UINT_SUCC c)) -> FALSE)) -> FALSE;
not_not_impl < (
assume ttt proves UINT_SATPRED (a++ - b) == a - b -> FALSE;
// Goal: FALSE
b_succ < (
// Goal:
// forany c: HAS_MEMBER UINT c -> (eq b (UINT_SUCC c)) -> FALSE
forany c:
assume cuint proves c : UINT;
assume b_sc proves b == c++;
// Goal: FALSE
ttt < (
// Goal:
// UINT_SATPRED (a++ - b) == a - b
require temp1 proves UINT_SATPRED (a - c) == UINT_SATPRED (a - c)
by eq_same;
require temp2 proves UINT_SATPRED (a - c) == a - c++
by temp1 > ((satsub_succ__satpred_satsub < auint < cuint) > eq_comm) > bin_sub_right_impl;
require temp3 proves UINT_SATPRED (a++ - c++) == a - c++
by temp2 > (((succ_satsub_succ < auint < cuint) > eq_comm) > un_sub_arg) > bin_sub_left_impl;
require temp4 proves UINT_SATPRED (a++ - b) == a - c++
by temp3 > (((b_sc > eq_comm) > bin_sub_right_eq) > un_sub_arg) > bin_sub_left_impl;
temp4 > ((b_sc > eq_comm) > bin_sub_right_eq) > bin_sub_right_impl
)
)
)
)
);
/*
require satsub_succ__satpred_satsub2 proves forany a,b: a : UINT -> b : UINT -> (a - b++) == UINT_SATPRED (a - b)
by (
forany a,b:
assume auint proves a : UINT;
assume buint proves b : UINT;
or_cases < (uint_is_zero_or_succ < auint) < (
assume a_0 proves a == UINT_ZERO;
require temp1 proves UINT_ZERO == UINT_SATPRED (UINT_ZERO - b)
by (sat_pred_zero_is_zero > eq_comm) > (((buint > zero_satsub) > eq_comm) > un_sub_arg) > bin_sub_right_impl;
require temp2 proves (UINT_ZERO - b++) == UINT_SATPRED (UINT_ZERO - b)
by temp1 > (((buint > succ_uint_is_uint) > zero_satsub) > eq_comm) > bin_sub_left_impl;
require temp3 proves (UINT_ZERO - b++) == UINT_SATPRED (a - b)
by temp2 > (((a_0 > eq_comm) > bin_sub_left_eq) > un_sub_arg) > bin_sub_right_impl;
temp3 > ((a_0 > eq_comm) > bin_sub_left_eq) > bin_sub_left_impl
) < (
assume a_succ proves (forany c: (HAS_MEMBER UINT c -> (eq a (UINT_SUCC c)) -> FALSE)) -> FALSE;
not_not_impl < (
assume ttt proves ((a - b++) == UINT_SATPRED (a - b)) -> FALSE;
// Goal: FALSE
a_succ < (
// Goal:
// forany c: (HAS_MEMBER UINT c -> (eq a (UINT_SUCC c)) -> FALSE)
forany c:
assume cuint proves c : UINT;
assume a_sc proves a == c++;
// Goal: FALSE
ttt < (
// Goal:
// (a - b++) == UINT_SATPRED (a - b)
require temp1 proves c - b == c - b by eq_same;
require temp2 proves (c - b) == UINT_SATPRED (c++ - b)
by temp1 > ((sat_pred__succ_satsub < cuint < buint) > eq_comm) > bin_sub_right_impl;
require temp3 proves (c++ - b++) == UINT_SATPRED (c++ - b)
by temp2 > ((succ_satsub_succ < cuint < buint) > eq_comm) > bin_sub_left_impl;
(temp3 > ((a_sc > eq_comm) > bin_sub_left_eq) > bin_sub_left_impl) > (((a_sc > eq_comm) > bin_sub_left_eq) > un_sub_arg) > bin_sub_right_impl
// (c - b) == (c - b)
// (c - b) == UINT_SATPRED (c++ - b)
// (c++ - b++) == UINT_SATPRED (c++ - b)
)
)
)
)
// (a - b++) == UINT_SATPRED (a - b)
);
*/
require UINT_ADD_switcheq proves forany a,b: UINT_ADD a b == SWITCH b UINT_ZERO a (UINT_SUCC (UINT_ADD a (UINT_PRED b)))
by (
forany a,b:
wrap eq (
impl_impl_and
< ( assume a1 proves UINT_ADD a b; unwrap a1 )
< ( assume a2 proves SWITCH b UINT_ZERO a (UINT_SUCC (UINT_ADD a (UINT_PRED b))); wrap UINT_ADD a2 )
)
);
require add_succ proves forany a,b: (a : UINT) -> (b : UINT) -> eq (UINT_ADD a (UINT_SUCC b)) (UINT_SUCC (a + b))
by (
forany a,b:
assume auint proves a : UINT;
assume buint proves b : UINT;
require temp1 proves (UINT_ADD a (UINT_SUCC b)) == (UINT_ADD a (UINT_SUCC b))
by eq_same;
require temp2 proves (UINT_ADD a (UINT_SUCC b)) == SWITCH (UINT_SUCC b) UINT_ZERO a (UINT_SUCC (UINT_ADD a (UINT_PRED (UINT_SUCC b))))
by temp1 > UINT_ADD_switcheq > bin_sub_right_impl;
require temp3 proves (UINT_ADD a (UINT_SUCC b)) == (UINT_SUCC (UINT_ADD a (UINT_PRED (UINT_SUCC b))))
by temp2 > (succ_not_zero > switch_no) > bin_sub_right_impl;
require temp4 proves (UINT_ADD a (UINT_SUCC b)) == (UINT_SUCC (UINT_ADD a b))
by temp3 > (((buint > uint_pred) > bin_sub_right_eq) > un_sub_arg) > bin_sub_right_impl;
temp4