File: induct.lisp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (3073 lines) | stat: -rw-r--r-- 134,699 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
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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2095
2096
2097
2098
2099
2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141
2142
2143
2144
2145
2146
2147
2148
2149
2150
2151
2152
2153
2154
2155
2156
2157
2158
2159
2160
2161
2162
2163
2164
2165
2166
2167
2168
2169
2170
2171
2172
2173
2174
2175
2176
2177
2178
2179
2180
2181
2182
2183
2184
2185
2186
2187
2188
2189
2190
2191
2192
2193
2194
2195
2196
2197
2198
2199
2200
2201
2202
2203
2204
2205
2206
2207
2208
2209
2210
2211
2212
2213
2214
2215
2216
2217
2218
2219
2220
2221
2222
2223
2224
2225
2226
2227
2228
2229
2230
2231
2232
2233
2234
2235
2236
2237
2238
2239
2240
2241
2242
2243
2244
2245
2246
2247
2248
2249
2250
2251
2252
2253
2254
2255
2256
2257
2258
2259
2260
2261
2262
2263
2264
2265
2266
2267
2268
2269
2270
2271
2272
2273
2274
2275
2276
2277
2278
2279
2280
2281
2282
2283
2284
2285
2286
2287
2288
2289
2290
2291
2292
2293
2294
2295
2296
2297
2298
2299
2300
2301
2302
2303
2304
2305
2306
2307
2308
2309
2310
2311
2312
2313
2314
2315
2316
2317
2318
2319
2320
2321
2322
2323
2324
2325
2326
2327
2328
2329
2330
2331
2332
2333
2334
2335
2336
2337
2338
2339
2340
2341
2342
2343
2344
2345
2346
2347
2348
2349
2350
2351
2352
2353
2354
2355
2356
2357
2358
2359
2360
2361
2362
2363
2364
2365
2366
2367
2368
2369
2370
2371
2372
2373
2374
2375
2376
2377
2378
2379
2380
2381
2382
2383
2384
2385
2386
2387
2388
2389
2390
2391
2392
2393
2394
2395
2396
2397
2398
2399
2400
2401
2402
2403
2404
2405
2406
2407
2408
2409
2410
2411
2412
2413
2414
2415
2416
2417
2418
2419
2420
2421
2422
2423
2424
2425
2426
2427
2428
2429
2430
2431
2432
2433
2434
2435
2436
2437
2438
2439
2440
2441
2442
2443
2444
2445
2446
2447
2448
2449
2450
2451
2452
2453
2454
2455
2456
2457
2458
2459
2460
2461
2462
2463
2464
2465
2466
2467
2468
2469
2470
2471
2472
2473
2474
2475
2476
2477
2478
2479
2480
2481
2482
2483
2484
2485
2486
2487
2488
2489
2490
2491
2492
2493
2494
2495
2496
2497
2498
2499
2500
2501
2502
2503
2504
2505
2506
2507
2508
2509
2510
2511
2512
2513
2514
2515
2516
2517
2518
2519
2520
2521
2522
2523
2524
2525
2526
2527
2528
2529
2530
2531
2532
2533
2534
2535
2536
2537
2538
2539
2540
2541
2542
2543
2544
2545
2546
2547
2548
2549
2550
2551
2552
2553
2554
2555
2556
2557
2558
2559
2560
2561
2562
2563
2564
2565
2566
2567
2568
2569
2570
2571
2572
2573
2574
2575
2576
2577
2578
2579
2580
2581
2582
2583
2584
2585
2586
2587
2588
2589
2590
2591
2592
2593
2594
2595
2596
2597
2598
2599
2600
2601
2602
2603
2604
2605
2606
2607
2608
2609
2610
2611
2612
2613
2614
2615
2616
2617
2618
2619
2620
2621
2622
2623
2624
2625
2626
2627
2628
2629
2630
2631
2632
2633
2634
2635
2636
2637
2638
2639
2640
2641
2642
2643
2644
2645
2646
2647
2648
2649
2650
2651
2652
2653
2654
2655
2656
2657
2658
2659
2660
2661
2662
2663
2664
2665
2666
2667
2668
2669
2670
2671
2672
2673
2674
2675
2676
2677
2678
2679
2680
2681
2682
2683
2684
2685
2686
2687
2688
2689
2690
2691
2692
2693
2694
2695
2696
2697
2698
2699
2700
2701
2702
2703
2704
2705
2706
2707
2708
2709
2710
2711
2712
2713
2714
2715
2716
2717
2718
2719
2720
2721
2722
2723
2724
2725
2726
2727
2728
2729
2730
2731
2732
2733
2734
2735
2736
2737
2738
2739
2740
2741
2742
2743
2744
2745
2746
2747
2748
2749
2750
2751
2752
2753
2754
2755
2756
2757
2758
2759
2760
2761
2762
2763
2764
2765
2766
2767
2768
2769
2770
2771
2772
2773
2774
2775
2776
2777
2778
2779
2780
2781
2782
2783
2784
2785
2786
2787
2788
2789
2790
2791
2792
2793
2794
2795
2796
2797
2798
2799
2800
2801
2802
2803
2804
2805
2806
2807
2808
2809
2810
2811
2812
2813
2814
2815
2816
2817
2818
2819
2820
2821
2822
2823
2824
2825
2826
2827
2828
2829
2830
2831
2832
2833
2834
2835
2836
2837
2838
2839
2840
2841
2842
2843
2844
2845
2846
2847
2848
2849
2850
2851
2852
2853
2854
2855
2856
2857
2858
2859
2860
2861
2862
2863
2864
2865
2866
2867
2868
2869
2870
2871
2872
2873
2874
2875
2876
2877
2878
2879
2880
2881
2882
2883
2884
2885
2886
2887
2888
2889
2890
2891
2892
2893
2894
2895
2896
2897
2898
2899
2900
2901
2902
2903
2904
2905
2906
2907
2908
2909
2910
2911
2912
2913
2914
2915
2916
2917
2918
2919
2920
2921
2922
2923
2924
2925
2926
2927
2928
2929
2930
2931
2932
2933
2934
2935
2936
2937
2938
2939
2940
2941
2942
2943
2944
2945
2946
2947
2948
2949
2950
2951
2952
2953
2954
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
2965
2966
2967
2968
2969
2970
2971
2972
2973
2974
2975
2976
2977
2978
2979
2980
2981
2982
2983
2984
2985
2986
2987
2988
2989
2990
2991
2992
2993
2994
2995
2996
2997
2998
2999
3000
3001
3002
3003
3004
3005
3006
3007
3008
3009
3010
3011
3012
3013
3014
3015
3016
3017
3018
3019
3020
3021
3022
3023
3024
3025
3026
3027
3028
3029
3030
3031
3032
3033
3034
3035
3036
3037
3038
3039
3040
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050
3051
3052
3053
3054
3055
3056
3057
3058
3059
3060
3061
3062
3063
3064
3065
3066
3067
3068
3069
3070
3071
3072
3073
; ACL2 Version 3.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2006  University of Texas at Austin

; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; Written by:  Matt Kaufmann               and J Strother Moore
; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

(in-package "ACL2")

(defun select-x-cl-set (cl-set induct-hint-val)

; This function produces the clause set we explore to collect
; induction candidates.  The x in this name means "explore."  If
; induct-hint-val is non-nil and non-t, we use the user-supplied
; induction hint value (which, if t means use cl-set); otherwise, we
; use cl-set.

  (cond ((null induct-hint-val) cl-set)
        ((equal induct-hint-val *t*) cl-set)
        (t (list (list induct-hint-val)))))

(defun unchangeables (formals args quick-block-info subset ans)

; We compute the set of all variable names occurring in args in
; unchanging measured formal positions.  We accumulate the answer onto
; ans.

  (cond ((null formals) ans)
        ((and (member-eq (car formals) subset)
              (eq (car quick-block-info) 'unchanging))
         (unchangeables (cdr formals) (cdr args) (cdr quick-block-info) subset
                        (all-vars1 (car args) ans)))
        (t
         (unchangeables (cdr formals) (cdr args) (cdr quick-block-info) subset
                        ans))))

(defun changeables (formals args quick-block-info subset ans)

; We compute the args in changing measured formal positions.  We
; accumulate the answer onto ans.

  (cond ((null formals) ans)
        ((and (member-eq (car formals) subset)
              (not (eq (car quick-block-info) 'unchanging)))
         (changeables (cdr formals) (cdr args) (cdr quick-block-info)
                      subset
                      (cons (car args) ans)))
        (t
         (changeables (cdr formals) (cdr args) (cdr quick-block-info)
                      subset
                      ans))))

(defun sound-induction-principle-mask1 (formals args quick-block-info
                                                subset
                                                unchangeables
                                                changeables)
; See sound-induction-principle-mask.

  (cond
   ((null formals) nil)
   (t (let ((var (car formals))
            (arg (car args))
            (q (car quick-block-info)))
        (mv-let (mask-ele new-unchangeables new-changeables)
          (cond ((member-eq var subset)
                 (cond ((eq q 'unchanging)
                        (mv 'unchangeable unchangeables changeables))
                       (t (mv 'changeable unchangeables changeables))))
                ((and (variablep arg)
                      (eq q 'unchanging))
                 (cond ((member-eq arg changeables)
                        (mv nil unchangeables changeables))
                       (t (mv 'unchangeable
                              (add-to-set-eq arg unchangeables)
                              changeables))))
                ((and (variablep arg)
                      (not (member-eq arg changeables))
                      (not (member-eq arg unchangeables)))
                 (mv 'changeable
                     unchangeables
                     (cons arg changeables)))
                (t (mv nil unchangeables changeables)))
          (cons mask-ele
                (sound-induction-principle-mask1 (cdr formals)
                                                 (cdr args)
                                                 (cdr quick-block-info)
                                                 subset
                                                 new-unchangeables
                                                 new-changeables)))))))

(defun sound-induction-principle-mask (term formals quick-block-info subset)

; Term is a call of some fn on some args.  The formals and
; quick-block-info are those of fn, and subset is one of fn's measured
; subset (a subset of formals).  We wish to determine, in the
; terminology of ACL, whether the induction applies to term.  If so we
; return a mask indicating how to build the substitutions for the
; induction from args and the machine for fn.  Otherwise we return
; nil.

; Let the changeables be those args that are in measured formal
; positions that sometimes change in the recursion.  Let the
; unchangeables be all of the variables occurring in measured actuals
; that never change in recursion.  The induction applies if
; changeables is a sequence of distinct variable names and has an
; empty intersection with unchangeables.

; If the induction is applicable then the substitutions should
; substitute for the changeables just as the recursion would, and hold
; each unchangeable fixed -- i.e., substitute each for itself.  With
; such substitutions it is possible to prove the measure lemmas
; analogous to those proved when justification of subset was stored,
; except that the measure is obtained by instantiating the measure
; term used in the justification by the measured actuals in unchanging
; slots.  Actual variables that are neither among the changeables or
; unchangeables may be substituted for arbitrarily.

; If the induction is applicable we return a mask with as many
; elements as there are args.  For each arg the mask contains either
; 'changeable, 'unchangeable, or nil.  'Changeable means the arg
; should be instantiated as specified in the recursion.  'Unchangeable
; means each var in the actual should be held fixed.  Nil means that
; the corresponding substitution pairs in the machine for the function
; should be ignored.

; Abstractly, this function builds the mask by first putting either
; 'changeable or 'unchangeable in each measured slot.  It then fills
; in the remaining slots from the left so as to permit the actual to
; be instantiated or held fixed as desired by the recursion, provided
; that in so doing it does not permit substitutions for previously
; allocated actuals.

  (let ((unchangeables
         (unchangeables formals (fargs term) quick-block-info subset nil))
        (changeables
         (changeables formals (fargs term) quick-block-info subset nil)))
    (cond ((or (not (no-duplicatesp-equal changeables))
               (not (all-variablep changeables))
               (intersectp-eq changeables unchangeables))
           nil)
          (t (sound-induction-principle-mask1 formals
                                              (fargs term)
                                              quick-block-info
                                              subset
                                              unchangeables
                                              changeables)))))


(defrec candidate
  (score controllers changed-vars unchangeable-vars
         tests-and-alists-lst justification induction-term other-terms
         xinduction-term xother-terms xancestry
         ttree)
  nil)

; This record is used to represent one of the plausible inductions that must be
; considered.  The SCORE represents some fairly artificial estimation of how
; many terms in the conjecture want this induction.  CONTROLLERS is the list of
; the controllers -- including unchanging controllers -- for all the inductions
; merged to form this one.  The CHANGED-VARS is a list of all those variables
; that will be instantiated (non-identically) in some induction hypotheses.
; Thus, CHANGED-VARS include both variables that actually contribute to why
; some measure goes down and variables like accumulators that are just along
; for the ride.  UNCHANGEABLE-VARS is a list of all those vars which may not be
; changed by any substitution if this induction is to be sound for the reasons
; specified.  TESTS-AND-ALISTS-LST is a list of TESTS-AND-ALISTS which
; indicates the case analysis for the induction and how the various induction
; hypotheses are obtained via substitutions.  JUSTIFICATION is the
; JUSTIFICATION that justifies this induction, and INDUCTION-TERM is the term
; that suggested this induction and from which you obtain the actuals to
; substitute into the template.  OTHER-TERMS are the induction-terms of
; candidates that have been merged into this one for heuristic reasons.

; Because of induction rules we can think of some terms being aliases for
; others.  We have to make a distinction between the terms in the conjecture
; that suggested an induction and the actual terms that suggested the
; induction.  For example, if an induction rule maps (fn x y) to (recur x y),
; then (recur x y) will be the INDUCTION-TERM because it suggested the
; induction and we will, perhaps, have to recover its induction machine or
; quick block information to implement various heuristics.  But we do not wish
; to report (recur x y) to the user, preferring instead to report (fn x y).
; Therefore, corresponding to INDUCTION-TERM and OTHER-TERMS we have
; XINDUCTION-TERM and XOTHER-TERMS, which are maintained in exactly the same
; way as their counterparts but which deal completely with the user-level view
; of the induction.  In practice this means that we will initialize the
; XINDUCTION-TERM field of a candidate with the term from the conjecture,
; initialize the INDUCTION-TERM with its alias, and then merge the fields
; completely independently but analogously.  XANCESTRY is a field maintained by
; merging to contain the user-level terms that caused us to change our
; tests-and-alists.  (Some candidates may be flushed or merged into this one
; without changing it.)

; The ttree of a candidate contains 'LEMMA tags listing the :induction rules
; (if any) involved in the suggestion of the candidate.

(defun count-non-nils (lst)
  (cond ((null lst) 0)
        ((car lst) (1+ (count-non-nils (cdr lst))))
        (t (count-non-nils (cdr lst)))))

(defun controllers (formals args subset ans)
  (cond ((null formals) ans)
        ((member (car formals) subset)
         (controllers (cdr formals) (cdr args) subset
                      (all-vars1 (car args) ans)))
        (t (controllers (cdr formals) (cdr args) subset ans))))

(defun changed/unchanged-vars (x args mask ans)
  (cond ((null mask) ans)
        ((eq (car mask) x)
         (changed/unchanged-vars x (cdr args) (cdr mask)
                                 (all-vars1 (car args) ans)))
        (t (changed/unchanged-vars x (cdr args) (cdr mask) ans))))

(defrec tests-and-alists (tests alists) nil)

(defun tests-and-alists/alist (alist args mask call-args)

; Alist is an alist that maps the formals of some fn to its actuals,
; args.  Mask is a sound-induction-principle-mask indicating the args
; for which we will build substitution pairs.  Call-args is the list of
; arguments to some recursive call of fn occurring in the induction
; machine for fn.  We build an alist mapping the masked args to the
; instantiations (under alist) of the values in call-args.

  (cond
   ((null mask) nil)
   ((null (car mask))
    (tests-and-alists/alist alist (cdr args) (cdr mask) (cdr call-args)))
   ((eq (car mask) 'changeable)
    (cons (cons (car args)
                (sublis-var alist (car call-args)))
          (tests-and-alists/alist alist
                                  (cdr args)
                                  (cdr mask)
                                  (cdr call-args))))
   (t (let ((vars (all-vars (car args))))
        (append (pairlis$ vars vars)
                (tests-and-alists/alist alist
                                        (cdr args)
                                        (cdr mask)
                                        (cdr call-args)))))))

(defun tests-and-alists/alists (alist args mask calls)

; Alist is an alist that maps the formals of some fn to its actuals,
; args.  Mask is a sound-induction-principle-mask indicating the args
; for which we will build substitution pairs.  Calls is the list of
; calls for a given case of the induction machine.  We build the alists
; from those calls.

  (cond
   ((null calls) nil)
   (t (cons (tests-and-alists/alist alist args mask (fargs (car calls)))
            (tests-and-alists/alists alist args mask (cdr calls))))))

; The following record contains the tests leading to a collection of
; recursive calls at the end of a branch through a defun.  In general,
; the calls may not be to the function being defuned but rather to
; some other function in the same mutually recursive clique, but in
; the context of induction we know that all the calls are to the same
; fn because we haven't implemented mutually recursive inductions yet.

; A list of these records constitute the induction machine for a function.

(defrec tests-and-calls (tests . calls) nil)

; The justification record contains a subset of the formals of the function
; under which it is stored.  Only the subset field has semantic content!  The
; other fields are the domain predicate, mp; the relation, rel, which is
; well-founded on mp objects; and the mp-measure term which has been proved to
; decrease in the recursion.  The latter three fields are correct at the time
; the function is admitted, but note that they might all be local and hence
; have disappeared by the time these fields are read.  Thus, we include them
; only for heuristic purposes, for example as used in
; books/workshops/2004/legato/support/generic-theories.lisp.

; A list of justification records is stored under each function symbol by the
; defun principle.

(defrec justification (subset mp rel measure) nil)

(defun tests-and-alists (alist args mask tc)

; Alist is an alist that maps the formals of some fn to its actuals,
; args.  Mask is a sound-induction-principle-mask indicating the args
; for which we will build substitution pairs.  Tc is one of the
; tests-and-calls in the induction machine for the function.  We make
; a tests-and-alists record containing the instantiated tests of tc
; and alists derived from the calls of tc.

  (make tests-and-alists
        :tests (sublis-var-lst alist (access tests-and-calls tc :tests))
        :alists (tests-and-alists/alists alist
                                        args
                                        mask
                                        (access tests-and-calls tc :calls))))

(defun tests-and-alists-lst (alist args mask machine)

; We build a list of tests-and-alists from machine, instantiating it
; with alist, which is a map from the formals of the function to the
; actuals, args.  Mask is the sound-induction-principle-mask that
; indicates the args for which we substitute.

  (cond
   ((null machine) nil)
   (t (cons (tests-and-alists alist args mask (car machine))
            (tests-and-alists-lst alist args mask (cdr machine))))))

(defun flesh-out-induction-principle (term formals justification mask machine
                                           xterm ttree)

; Term is a call of some function the indicated formals and induction machine.
; Justification is its 'justification and mask is a sound-induction-
; principle-mask for the term.  We build the induction candidate suggested by
; term.

  (make candidate
        :score
        (/ (count-non-nils mask) (length mask))

        :controllers
        (controllers formals (fargs term)
                     (access justification justification :subset)
                     nil)

        :changed-vars
        (changed/unchanged-vars 'changeable (fargs term) mask nil)

        :unchangeable-vars
        (changed/unchanged-vars 'unchangeable (fargs term) mask nil)

        :tests-and-alists-lst
        (tests-and-alists-lst (pairlis$ formals (fargs term))
                              (fargs term) mask machine)

        :justification justification

        :induction-term term
        :xinduction-term xterm

        :other-terms nil
        :xother-terms nil
        :xancestry nil
        :ttree ttree))

(defun intrinsic-suggested-induction-cand
  (term formals quick-block-info justification machine xterm ttree ens wrld)

; Note: An "intrinsically suggested" induction scheme is an induction scheme
; suggested by a justification of a recursive function.  The rune controlling
; the intrinsic suggestion from the justification of fn is (:induction fn).  We
; distinguish between intrinsically suggested inductions and those suggested
; via records of induction-rule type.  Intrinsic inductions have no embodiment
; as induction-rules but are, instead, the basis of the semantics of such
; rules.  That is, the inductions suggested by (fn x y) is the union of those
; suggested by the terms to which it is linked via induction-rules together
; with the intrinsic suggestion for (fn x y).

; Term, above, is a call of some fn with the given formals, quick-block-info,
; justification and induction machine.  We return a list of induction
; candidates, said list either being empty or the singleton list containing the
; induction candidate intrinsically suggested by term.  Xterm is logically
; unrelated to term and is the term appearing in the original conjecture from
; which we (somehow) obtained term for consideration.

  (let ((induction-rune (list :induction (ffn-symb term))))
    (cond
     ((enabled-runep induction-rune ens wrld)
      (let ((mask (sound-induction-principle-mask term formals
                                                  quick-block-info
                                                  (access justification
                                                          justification
                                                          :subset))))
        (cond
         (mask
          (list (flesh-out-induction-principle term formals
                                               justification
                                               mask
                                               machine
                                               xterm
                                               (push-lemma induction-rune
                                                           ttree))))
         (t nil))))
     (t nil))))

(defrec induction-rule (nume (pattern . condition) scheme . rune) nil)

(mutual-recursion

(defun apply-induction-rule (rule term type-alist xterm ttree ens wrld)

; We apply the induction-rule, rule, to term, and return a possibly empty list
; of suggested inductions.  The basic idea is to check that the rule is enabled
; and that the :pattern of the rule matches term.  If so, we check that the
; :condition of the rule is true under the current type-alist.  This check is
; heuristic only and so we indicate that the guards have been checked and we
; allow forcing.  We ignore the ttree because we are making a heuristic choice
; only.  If type-set says the :condition is non-nil, we fire the rule by
; instantiating the :scheme and recursively getting the suggested inductions
; for that term.  Note that we are not recursively exploring the instantiated
; scheme but just getting the inductions suggested by its top-level function
; symbol.

  (cond
   ((enabled-numep (access induction-rule rule :nume) ens)
    (mv-let
     (ans alist)
     (one-way-unify (access induction-rule rule :pattern)
                    term)
     (cond
      (ans
       (with-accumulated-persistence
        (access induction-rule rule :rune)
        (suggestions)
        (mv-let
         (ts ttree1)
         (type-set (sublis-var alist
                               (access induction-rule rule :condition))
                   t nil type-alist nil ens wrld nil
                   nil nil)
         (declare (ignore ttree1))
         (cond
          ((ts-intersectp *ts-nil* ts) nil)
          (t (let ((term1 (sublis-var alist
                                      (access induction-rule rule :scheme))))
               (cond ((or (variablep term1)
                          (fquotep term1))
                      nil)
                     (t (suggested-induction-cands term1 type-alist
                                                   xterm
                                                   (push-lemma
                                                    (access induction-rule
                                                            rule
                                                            :rune)
                                                    ttree)
                                                   ens wrld)))))))))
      (t nil))))
   (t nil)))

(defun suggested-induction-cands1
  (induction-rules term type-alist xterm ttree ens wrld)

; We map down induction-rules and apply each enabled rule to term, which is
; known to be an application of the function symbol fn to some args.  Each rule
; gives us a possibly empty list of suggested inductions.  We append all these
; suggestions together.  In addition, if fn is recursively defined and is
; enabled (or, even if fn is disabled if we are exploring a user-supplied
; induction hint) we collect the intrinsic suggestion for term as well.

  (cond
   ((null induction-rules)
    (let* ((fn (ffn-symb term))
           (machine (getprop fn 'induction-machine nil
                             'current-acl2-world wrld)))
      (cond
       ((null machine) nil)
       (t

; Historical note:  Before Version_2.6 we had the following note:

;   Note: The intrinsic suggestion will be non-nil only if (:INDUCTION fn) is
;   enabled and so here we have a case in which two runes have to be enabled
;   (the :DEFINITION and the :INDUCTION runes) to get the desired effect.  It
;   is not clear if this is a good design but at first sight it seems to
;   provide upward compatibility because in Nqthm a disabled function suggests
;   no inductions.

; We no longer make any such requirement:  the test above (t) replaces the
; following.

;       (or (enabled-fnp fn nil ens wrld)
;           (and induct-hint-val
;                (not (equal induct-hint-val *t*))))

        (intrinsic-suggested-induction-cand
         term
         (formals fn wrld)
         (getprop fn 'quick-block-info
                  '(:error "See SUGGESTED-INDUCTION-CANDS1.")
                  'current-acl2-world wrld)
         (getprop fn 'justification
                  '(:error "See SUGGESTED-INDUCTION-CANDS1.")
                  'current-acl2-world wrld)
         machine
         xterm
         ttree
         ens
         wrld)))))
   (t (append (apply-induction-rule (car induction-rules)
                                    term type-alist
                                    xterm ttree ens wrld)
              (suggested-induction-cands1 (cdr induction-rules)
                                          term type-alist
                                          xterm ttree ens wrld)))))

(defun suggested-induction-cands
  (term type-alist xterm ttree ens wrld)

; Term is some fn applied to args.  Xterm is some term occurring in the
; conjecture we are exploring and is the term upon which this induction
; suggestion will be "blamed" and from which we have obtained term via
; induction-rules.  We return all of the induction candidates suggested by
; term.  Lambda applications suggest no inductions.  Disabled functions suggest
; no inductions -- unless we are applying the user's induct hint value (in
; which case we, quite reasonably, assume every function in the value is worthy
; of analysis since any function could have been omitted).

  (cond
   ((flambdap (ffn-symb term)) nil)
   (t (suggested-induction-cands1
       (getprop (ffn-symb term) 'induction-rules nil 'current-acl2-world wrld)
       term type-alist xterm ttree ens wrld))))
)

(mutual-recursion

(defun get-induction-cands (term type-alist ens wrld ans)

; We explore term and accumulate onto ans all of the induction
; candidates suggested by it.

  (cond ((variablep term) ans)
        ((fquotep term) ans)
        ((eq (ffn-symb term) 'hide)
         ans)
        (t (get-induction-cands-lst
            (fargs term)
            type-alist ens wrld
            (append (suggested-induction-cands term type-alist
                                               term nil ens wrld)
                    ans)))))

(defun get-induction-cands-lst (lst type-alist ens wrld ans)

; We explore the list of terms, lst, and accumulate onto ans all of
; the induction candidates.

  (cond ((null lst) ans)
        (t (get-induction-cands
            (car lst)
            type-alist ens wrld
            (get-induction-cands-lst
             (cdr lst)
             type-alist ens wrld ans)))))

)

(defun get-induction-cands-from-cl-set1 (cl-set ens oncep-override wrld state
                                                ans)

; We explore cl-set and accumulate onto ans all of the induction
; candidates.

  (cond
   ((null cl-set) ans)
   (t (mv-let (contradictionp type-alist fc-pairs)
              (forward-chain (car cl-set) nil t
                             nil ; do-not-reconsiderp
                             wrld ens oncep-override state)

; We need a type-alist with which to compute induction aliases.  It is of
; heuristic use only, so we may as well turn the force-flg on.  We assume no
; contradiction is found.  If by chance one is, then type-alist is nil, which
; is an acceptable type-alist.

              (declare (ignore contradictionp fc-pairs))
              (get-induction-cands-lst
               (car cl-set)
               type-alist ens wrld
               (get-induction-cands-from-cl-set1 (cdr cl-set)
                                                 ens oncep-override wrld state
                                                 ans))))))

(defun get-induction-cands-from-cl-set (cl-set pspv wrld state)

; We explore cl-set and collect all induction candidates.

  (let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
    (get-induction-cands-from-cl-set1 cl-set
                                      (access rewrite-constant
                                              rcnst
                                              :current-enabled-structure)
                                      (access rewrite-constant
                                              rcnst
                                              :oncep-override)
                                      wrld
                                      state
                                      nil)))

; That completes the development of the code for exploring a clause set
; and gathering the induction candidates suggested.

; Section:  Pigeon-Holep

; We next develop pigeon-holep, which tries to fit some "pigeons" into
; some "holes" using a function to determine the sense of the word
; "fit".  Since ACL2 is first-order we can't pass arbitrary functions
; and hence we pass symbols and define our own special-purpose "apply"
; that interprets the particular symbols passed to calls of
; pigeon-holep.

; However, it turns out that the applications of pigeon-holep require
; passing functions that themselves call pigeon-holep.  And so
; pigeon-holep-apply is mutually recursive with pigeon-holep (but only
; because the application functions use pigeon-holep).

(mutual-recursion

(defun pigeon-holep-apply (fn pigeon hole)

; See pigeon-holep for the problem and terminology.  This function
; takes a symbol denoting a predicate and two arguments.  It applies
; the predicate to the arguments.  When the predicate holds we say
; the pigeon argument "fits" into the hole argument.

  (case fn
        (pair-fitp

; This predicate is applied to two pairs, each taken from two substitutions.
; We say (v1 . term1) (the "pigeon") fits into (v2 . term2) (the "hole")
; if v1 is v2 and term1 occurs in term2.

         (and (eq (car pigeon) (car hole))
              (occur (cdr pigeon) (cdr hole))))

        (alist-fitp

; This predicate is applied to two substitutions. We say the pigeon
; alist fits into the hole alist if each pair of the pigeon fits into
; a pair of the hole and no pair of the hole is used more than once.

         (pigeon-holep pigeon hole nil 'pair-fitp))

        (tests-and-alists-fitp

; This predicate is applied to two tests-and-alists records.  The
; first fits into the second if the tests of the first are a subset
; of those of the second and either they are both base cases (i.e., have
; no alists) or each substitution of the first fits into a substitution of
; the second, using no substitution of the second more than once.

         (and (subsetp-equal (access tests-and-alists pigeon :tests)
                             (access tests-and-alists hole :tests))
              (or (and (null (access tests-and-alists pigeon :alists))
                       (null (access tests-and-alists hole :alists)))
                  (pigeon-holep (access tests-and-alists pigeon :alists)
                                (access tests-and-alists hole :alists)
                                nil
                                'alist-fitp))))))

(defun pigeon-holep (pigeons holes filled-holes fn)

; Both pigeons and holes are lists of arbitrary objects.  The holes
; are implicitly enumerated left-to-right from 0.  Filled-holes is a
; list of the indices of holes we consider "filled."  Fn is a
; predicate known to pigeon-holep-apply.  If fn applied to a pigeon and
; a hole is non-nil, then we say the pigeon "fits" into the hole.  We
; can only "put" a pigeon into a hole if the hole is unfilled and the
; pigeon fits.  The act of putting the pigeon into the hole causes the
; hole to become filled.  We return t iff it is possible to put each
; pigeon into a hole under these rules.

  (cond
   ((null pigeons) t)
   (t (pigeon-holep1 (car pigeons)
                     (cdr pigeons)
                     holes 0
                     holes filled-holes fn))))

(defun pigeon-holep1 (pigeon pigeons lst n holes filled-holes fn)

; Lst is a terminal sublist of holes, whose first element has index n.
; We map over lst looking for an unfilled hole h such that (a) we can
; put pigeon into h and (b) we can dispose of the rest of the pigeons
; after filling h.

  (cond
   ((null lst) nil)
   ((member n filled-holes)
    (pigeon-holep1 pigeon pigeons (cdr lst) (1+ n) holes filled-holes fn))
   ((and (pigeon-holep-apply fn pigeon (car lst))
         (pigeon-holep pigeons holes
                       (cons n filled-holes)
                       fn))
    t)
   (t (pigeon-holep1 pigeon pigeons (cdr lst) (1+ n)
                     holes filled-holes fn))))

)

(defun flush-cand1-down-cand2 (cand1 cand2)

; This function takes two induction candidates and determines whether
; the first is subsumed by the second.  If so, it constructs a new
; candidate that is logically equivalent (vis a vis the induction
; suggested) to the second but which now carries with it the weight
; and heuristic burdens of the first.

  (cond
   ((and (subsetp-eq (access candidate cand1 :changed-vars)
                     (access candidate cand2 :changed-vars))
         (subsetp-eq (access candidate cand1 :unchangeable-vars)
                     (access candidate cand2 :unchangeable-vars))
         (pigeon-holep (access candidate cand1 :tests-and-alists-lst)
                       (access candidate cand2 :tests-and-alists-lst)
                       nil
                       'tests-and-alists-fitp))
    (change candidate cand2
            :score (+ (access candidate cand1 :score)
                      (access candidate cand2 :score))
            :controllers (union-eq (access candidate cand1 :controllers)
                                   (access candidate cand2 :controllers))
            :other-terms (add-to-set-equal
                          (access candidate cand1 :induction-term)
                          (union-equal
                           (access candidate cand1 :other-terms)
                           (access candidate cand2 :other-terms)))
            :xother-terms (add-to-set-equal
                           (access candidate cand1 :xinduction-term)
                           (union-equal
                            (access candidate cand1 :xother-terms)
                            (access candidate cand2 :xother-terms)))
            :ttree (cons-tag-trees (access candidate cand1 :ttree)
                                   (access candidate cand2 :ttree))))
   (t nil)))

(defun flush-candidates (cand1 cand2)

; This function determines whether one of the two induction candidates
; given flushes down the other and if so returns the appropriate
; new candidate.  This function is a mate and merge function used
; by m&m and is hence known to m&m-apply.

  (or (flush-cand1-down-cand2 cand1 cand2)
      (flush-cand1-down-cand2 cand2 cand1)))

; We now begin the development of the merging of two induction
; candidates.  The basic idea is that if two functions both replace x
; by x', and one of them simultaneously replaces a by a' while the
; other replaces b by b', then we should consider inducting on x, a,
; and b, by x', a', and b'.  Of course, by the time we get here, the
; recursion is coded into substitution alists: ((x . x') (a . a')) and
; ((x . x') (b . b')).  We merge these two alists into ((x . x') (a .
; a') (b . b')).  The merge of two sufficiently compatible alists is
; accomplished by just unioning them together.

; The key ideas are (1) recognizing when two alists are describing the
; "same" recursive step (i.e., they are both replacing x by x', where
; x is somehow a key variable); (2) observing that they do not
; explicitly disagree on what to do with the other variables.

(defun alists-agreep (alist1 alist2 vars)

; Two alists agree on vars iff for each var in vars the image of var under
; the first alist is equal to that under the second.

  (cond ((null vars) t)
        ((equal (let ((temp (assoc-eq (car vars) alist1)))
                  (cond (temp (cdr temp))(t (car vars))))
                (let ((temp (assoc-eq (car vars) alist2)))
                  (cond (temp (cdr temp))(t (car vars)))))
         (alists-agreep alist1 alist2 (cdr vars)))
        (t nil)))

(defun irreconcilable-alistsp (alist1 alist2)

; Two alists are irreconcilable iff there is a var v that they both
; explicitly map to different values.  Put another way, there exists a
; v such that (v . a) is a member of alist1 and (v . b) is a member of
; alist2, where a and b are different.  If two substitutions are
; reconcilable then their union is a substitution.

; We rely on the fact that this function return t or nil.

  (cond ((null alist1) nil)
        (t (let ((temp (assoc-eq (caar alist1) alist2)))
             (cond ((null temp)
                    (irreconcilable-alistsp (cdr alist1) alist2))
                   ((equal (cdar alist1) (cdr temp))
                    (irreconcilable-alistsp (cdr alist1) alist2))
                   (t t))))))

(defun affinity (aff alist1 alist2 vars)

; We say two alists that agree on vars but are irreconcilable are
; "antagonists".  Two alists that agree on vars and are not irreconcilable
; are "mates".

; Aff is either 'antagonists or 'mates and denotes one of the two relations
; above.  We return t iff the other args are in the given relation.

  (and (alists-agreep alist1 alist2 vars)
       (eq (irreconcilable-alistsp alist1 alist2)
           (eq aff 'antagonists))))

(defun member-affinity (aff alist alist-lst vars)

; We determine if some member of alist-lst has the given affinity with alist.

  (cond ((null alist-lst) nil)
        ((affinity aff alist (car alist-lst) vars)
         t)
        (t (member-affinity aff alist (cdr alist-lst) vars))))

(defun occur-affinity (aff alist lst vars)

; Lst is a list of tests-and-alists.  We determine whether alist has
; the given affinity with some alist in lst.  We call this occur
; because we are looking inside the elements of lst.  But it is
; technically a misnomer because we don't look inside recursively; we
; treat lst as though it were a list of lists.

  (cond
   ((null lst) nil)
   ((member-affinity aff alist
                     (access tests-and-alists (car lst) :alists)
                     vars)
    t)
   (t (occur-affinity aff alist (cdr lst) vars))))

(defun some-occur-affinity (aff alists lst vars)

; Lst is a list of tests-and-alists.  We determine whether some alist
; in alists has the given affinity with some alist in lst.

  (cond ((null alists) nil)
        (t (or (occur-affinity aff (car alists) lst vars)
               (some-occur-affinity aff (cdr alists) lst vars)))))

(defun all-occur-affinity (aff alists lst vars)

; Lst is a list of tests-and-alists.  We determine whether every alist
; in alists has the given affinity with some alist in lst.

  (cond ((null alists) t)
        (t (and (occur-affinity aff (car alists) lst vars)
                (all-occur-affinity aff (cdr alists) lst vars)))))

(defun contains-affinity (aff lst vars)

; We determine if two members of lst have the given affinity.

  (cond ((null lst) nil)
        ((member-affinity aff (car lst) (cdr lst) vars) t)
        (t (contains-affinity aff (cdr lst) vars))))

; So much for general-purpose scanners.  We now develop the predicates
; that are used to determine if we can merge lst1 into lst2 on vars.
; See merge-tests-and-alists-lsts for extensive comments on the ideas
; behind the following functions.

(defun antagonistic-tests-and-alists-lstp (lst vars)

; Lst is a list of tests-and-alists.  Consider just the set of all
; alists in lst.  We return t iff that set contains an antagonistic
; pair.

; We operate as follows.  Each element of lst contains some alists.
; We take the first element and ask whether its alists contain an
; antagonistic pair.  If so, we're done.  Otherwise, we ask whether
; any alist in that first element is antagonistic with the alists in
; the rest of lst.  If so, we're done.  Otherwise, we recursively
; look at the rest of lst.

  (cond
   ((null lst) nil)
   (t (or (contains-affinity
           'antagonists
           (access tests-and-alists (car lst) :alists)
           vars)
          (some-occur-affinity
           'antagonists
           (access tests-and-alists (car lst) :alists)
           (cdr lst)
           vars)
          (antagonistic-tests-and-alists-lstp (cdr lst) vars)))))

(defun antagonistic-tests-and-alists-lstsp (lst1 lst2 vars)

; Both lst1 and lst2 are lists of tests-and-alists.  We determine whether
; there exists an alist1 in lst1 and an alist2 in lst2 such that alist1
; and alist2 are antagonists.

  (cond
   ((null lst1) nil)
   (t (or (some-occur-affinity
           'antagonists
           (access tests-and-alists (car lst1) :alists)
           lst2
           vars)
          (antagonistic-tests-and-alists-lstsp (cdr lst1) lst2 vars)))))

(defun every-alist1-matedp (lst1 lst2 vars)

; Both lst1 and lst2 are lists of tests-and-alists.  We determine for every
; alist1 in lst1 there exists an alist2 in lst2 that agrees with alist1 on
; vars and that is not irreconcilable.

  (cond ((null lst1) t)
        (t (and (all-occur-affinity
                 'mates
                 (access tests-and-alists (car lst1) :alists)
                 lst2
                 vars)
                (every-alist1-matedp (cdr lst1) lst2 vars)))))

; The functions above are used to determine that lst1 and lst2 contain
; no antagonistic pairs, that every alist in lst1 has a mate somewhere in
; lst2, and that the process of merging alists from lst1 with their
; mates will not produce alists that are antagonistic with other alists
; in lst1.  We now develop the code for merging nonantagonistic alists
; and work up the structural hierarchy to merging lists of tests and alists.

(defun merge-alist1-into-alist2 (alist1 alist2 vars)

; We assume alist1 and alist2 are not antagonists.  Thus, either they
; agree on vars and have no explicit disagreements, or they simply
; don't agree on vars.  If they agree on vars, we merge alist1 into
; alist2 by just unioning them together.  If they don't agree on vars,
; then we merge alist1 into alist2 by ignoring alist1.

  (cond
   ((alists-agreep alist1 alist2 vars)
    (union-equal alist1 alist2))
   (t alist2)))

; Now we begin working up the structural hierarchy.  Our strategy is
; to focus on a given alist2 and hit it with every alist1 we have.
; Then we'll use that to copy lst2 once, hitting each alist2 in it
; with everything we have.  We could decompose the problem the other
; way: hit lst2 with successive alist1's.  That suffers from forcing
; us to copy lst2 repeatedly, and there are parts of that structure
; (i.e., the :tests) that don't change.

(defun merge-alist1-lst-into-alist2 (alist1-lst alist2 vars)

; Alist1-lst is a list of alists and alist2 is an alist.  We know that
; there is no antagonists between the elements of alist1-lst and in
; alist2.  We merge each alist1 into alist2 and return
; the resulting extension of alist2.

  (cond
   ((null alist1-lst) alist2)
   (t (merge-alist1-lst-into-alist2
       (cdr alist1-lst)
       (merge-alist1-into-alist2 (car alist1-lst) alist2 vars)
       vars))))

(defun merge-lst1-into-alist2 (lst1 alist2 vars)

; Given a list of tests-and-alists, lst1, and an alist2, we hit alist2
; with every alist1 in lst1.

  (cond ((null lst1) alist2)
        (t (merge-lst1-into-alist2
            (cdr lst1)
            (merge-alist1-lst-into-alist2
             (access tests-and-alists (car lst1) :alists)
             alist2
             vars)
            vars))))

; So now we write the code to copy lst2, hitting each alist in it with lst1.

(defun merge-lst1-into-alist2-lst (lst1 alist2-lst vars)
  (cond ((null alist2-lst) nil)
        (t (cons (merge-lst1-into-alist2 lst1 (car alist2-lst) vars)
                 (merge-lst1-into-alist2-lst lst1 (cdr alist2-lst) vars)))))

(defun merge-lst1-into-lst2 (lst1 lst2 vars)
  (cond ((null lst2) nil)
        (t (cons (change tests-and-alists (car lst2)
                         :alists
                         (merge-lst1-into-alist2-lst
                          lst1
                          (access tests-and-alists (car lst2) :alists)
                          vars))
                 (merge-lst1-into-lst2 lst1 (cdr lst2) vars)))))

(defun merge-tests-and-alists-lsts (lst1 lst2 vars)

; Lst1 and lst2 are each tests-and-alists-lsts from some induction
; candidates.  Intuitively, we try to stuff the alists of lst1 into
; those of lst2 to construct a new lst2 that combines the induction
; schemes of both.  If we fail we return nil.  Otherwise we return the
; modified lst2.  The modified lst2 has exactly the same tests as
; before; only its alists are different and they are different only by
; virtue of having been extended with some addition pairs.  So the
; justification of the merged induction is the same as the
; justification of the original lst2.

; Given an alist1 from lst1, which alist2's of lst2 do you extend and
; how?  Suppose alist1 maps x to x' and y to y'.  Then intuitively we
; think "the first candidate is trying to keep x and y in step, so
; that when x goes to x' y goes to y'."  So, if you see an alist in
; lst2 that is replacing x by x', one might be tempted to augment it
; by replacing y by y'.  However, what if x is just an accumulator?
; The role of vars is to specify upon which variables two
; substitutions must agree in order to be merged.  Usually, vars
; consists of the measured variables.

; So now we get a little more technical.  We will try to "merge" each
; alist1 from lst1 into each alist2 from lst2 (preserving the case structure
; of lst2).  If alist1 and alist2 do not agree on vars then their merge
; is just alist2.  If they do agree on vars, then their merge is their
; union, provided that is a substitution.  It may fail to be a substitution
; because the two alists disagree on some other variable.  In that case
; we say the two are irreconcilable.  We now give three simple examples:

; Let vars be {x}.  Let alist2 be {(x . x') (z . z')}.  If alist1 maps
; x to x'', then their merge is just alist2 because alist1 is
; addressing a different case of the induction.  If alist1 maps x to x'
; and y to y', then their merge is {(x . x') (y . y') (z . z')}.  If
; alist1 maps x to x' and z to z'', then the two are irreconcilable.
; Two irreconcilable alists that agree on vars are called "antagonists"
; because they "want" to merge but can't.  We cannot merge lst1 into lst2
; if they have an antagonistic pair between them.  If an antagonistic pair
; is discovered, the entire merge operation fails.

; Now we will successively consider each alist1 in lst1 and merge it
; into lst2, forming successive lst2's.  We insist that each alist1 of
; lst1 have at least one mate in lst2 with which it agrees and is
; reconcilable.  (Otherwise, we could merge completely disjoint
; substitutions.)

; Because we try the alist1's successively, each alist1 is actually
; merged into the lst2 produced by all the previous alist1's.  That
; produces an apparent order dependence.  However, this is avoided by
; the requirement that we never produce antagonistic pairs.

; For example, suppose that in one case of lst1, x is mapped to x' and
; y is mapped to y', but in another case x is mapped to x' and y is
; mapped to y''.  Now imagine trying to merge that lst1 into a lst2 in
; which x is mapped to x' and z is mapped to z'.  The first alist of
; lst1 extends lst2 to (((x . x') (y . y') (z . z'))).  But the second
; alist is then antagonistic.  The same thing happens if we tried the two
; alists of lst1 in the other order.  Thus, the above lst1 cannot be merged
; into lst2.  Note that they can be merged in the other order!  That is,
; lst2 can be merged into lst1, because the case structure of lst1 is
; richer.

; We can detect the situation above without forming the intermediate
; lst2.  In particular, if lst1 contains an antagonistic pair, then it
; cannot be merged with any lst2 and we can quit.

; Note: Once upon a time, indeed, for the first 20 years or so of the
; existence of the merge routine, we took the attitude that if
; irreconcilable but agreeable alists arose, then we just added to
; alist2 those pairs of alist1 that were reconcilable and we left out
; the irreconcilable pairs.  This however resulted in the system often
; merging complicated accumulator using functions (like TAUTOLOGYP)
; into simpler functions (like NORMALIZEDP) by dropping the
; accumulators that got in the way.  This idea of just not doing
; "hostile merges" is being tried out for the first time in ACL2.

  (cond ((antagonistic-tests-and-alists-lstp lst1 vars) nil)
        ((antagonistic-tests-and-alists-lstsp lst1 lst2 vars) nil)
        ((not (every-alist1-matedp lst1 lst2 vars)) nil)
        (t (merge-lst1-into-lst2 lst1 lst2 vars))))

(defun merge-cand1-into-cand2 (cand1 cand2)

; Can induction candidate cand1 be merged into cand2?  If so, return
; their merge.  The guts of this function is merge-tests-and-alists-
; lsts.  The tests preceding it are heuristic only.  If
; merge-tests-and-alists-lsts returns non-nil, then it returns a sound
; induction; indeed, it merely extends some of the substitutions in
; the second candidate.

  (let ((vars (or (intersection-eq
                   (access candidate cand1 :controllers)
                   (intersection-eq
                    (access candidate cand2 :controllers)
                    (intersection-eq
                     (access candidate cand1 :changed-vars)
                     (access candidate cand2 :changed-vars))))
                  (intersection-eq
                   (access candidate cand1 :changed-vars)
                   (access candidate cand2 :changed-vars)))))

; Historical Plaque from Nqthm:

; We once merged only if both cands agreed on the intersection of the
; changed-vars.  But the theorem that, under suitable conditions, (EV
; FLG X VA FA N) = (EV FLG X VA FA K) made us realize it was important
; only to agree on the intersection of the controllers.  Note in fact
; that we mean the changing controllers -- there seems to be no need
; to merge two inductions if they only share unchanging controllers.
; However the theorem that (GET I (SET J VAL MEM)) = ... (GET I MEM)
; ...  illustrates the situation in which the controllers, {I} and {J}
; do not even overlap; but the accumulators {MEM} do and we want a
; merge.  So we want agreement on the intersection of the changing
; controllers (if that is nonempty) or on the accumulators.

; For soundness it does not matter what list of vars we want to agree
; on because no matter what, merge-tests-and-alists-lsts returns
; either nil or an extension of the second candidate's alists.

    (cond
     ((and vars
           (not (intersectp-eq (access candidate cand1 :unchangeable-vars)
                               (access candidate cand2 :changed-vars)))
           (not (intersectp-eq (access candidate cand2 :unchangeable-vars)
                               (access candidate cand1 :changed-vars))))
      (let ((temp (merge-tests-and-alists-lsts
                   (access candidate cand1 :tests-and-alists-lst)
                   (access candidate cand2 :tests-and-alists-lst)
                   vars)))
        (cond (temp
               (make candidate
                     :score (+ (access candidate cand1 :score)
                               (access candidate cand2 :score))
                     :controllers (union-eq
                                   (access candidate cand1 :controllers)
                                   (access candidate cand2 :controllers))
                     :changed-vars (union-eq
                                    (access candidate cand1 :changed-vars)
                                    (access candidate cand2 :changed-vars))
                     :unchangeable-vars (union-eq
                                         (access candidate cand1
                                                 :unchangeable-vars)
                                         (access candidate cand2
                                                 :unchangeable-vars))
                     :tests-and-alists-lst temp
                     :justification (access candidate cand2 :justification)
                     :induction-term (access candidate cand2 :induction-term)
                     :other-terms (add-to-set-equal
                                   (access candidate cand1 :induction-term)
                                   (union-equal
                                    (access candidate cand1 :other-terms)
                                    (access candidate cand2 :other-terms)))
                     :xinduction-term (access candidate cand2 :xinduction-term)
                     :xother-terms (add-to-set-equal
                                    (access candidate cand1 :xinduction-term)
                                    (union-equal
                                     (access candidate cand1 :xother-terms)
                                     (access candidate cand2 :xother-terms)))
                     :xancestry (cond
                                ((equal temp
                                        (access candidate cand2
                                                :tests-and-alists-lst))
                                 (access candidate cand2 :xancestry))
                                (t (add-to-set-equal
                                    (access candidate cand1 :xinduction-term)
                                    (union-equal
                                     (access candidate cand1 :xancestry)
                                     (access candidate cand2 :xancestry)))))

; Note that :xancestry, computed just above, may not reflect cand1, but we
; always include the :ttree of cand1 just below.  This is deliberate, since
; cand1 is contributing to the :score, and hence the eventual induction scheme
; chosen; so we want to report its induction rules in the final proof.

                     :ttree (cons-tag-trees (access candidate cand1 :ttree)
                                            (access candidate cand2 :ttree))))
              (t nil))))
     (t nil))))

(defun merge-candidates (cand1 cand2)

; This function determines whether one of the two induction candidates
; can be merged into the other.  If so, it returns their merge.  This
; function is a mate and merge function used by m&m and is hence known
; to m&m-apply.

  (or (merge-cand1-into-cand2 cand1 cand2)
      (merge-cand1-into-cand2 cand2 cand1)))

; We now move from merging to flawing.  The idea is to determine which
; inductions get in the way of others.



(defun controller-variables1 (args controller-pocket)

; Controller-pocket is a list of t's and nil's in 1:1 correspondence with
; args, indicating which args are controllers.  We collect those controller
; args that are variable symbols.

  (cond ((null controller-pocket) nil)
        ((and (car controller-pocket)
              (variablep (car args)))
         (add-to-set-eq (car args)
                        (controller-variables1 (cdr args)
                                               (cdr controller-pocket))))
        (t (controller-variables1 (cdr args)
                                  (cdr controller-pocket)))))

(defun controller-variables (term controller-alist)

; Controller-alist comes from the def-body of the function symbol, fn, of term.
; Recall that controller-alist is an alist that associates with each function
; in fn's mutually recursive clique the controller pockets used in a given
; justification of the clique.  In induction, as things stand today, we know
; that fn is singly recursive because we don't know how to handle mutual
; recursion yet.  But no use is made of that here.  We collect all the
; variables in controller slots of term.

  (controller-variables1 (fargs term)
                         (cdr (assoc-eq (ffn-symb term)
                                        controller-alist))))

(defun induct-vars1 (lst wrld)

; Lst is a list of terms.  We collect every variable symbol occuring in a
; controller slot of any term in lst.

  (cond ((null lst) nil)
        (t (union-eq
            (controller-variables
             (car lst)
             (access def-body
                     (def-body (ffn-symb (car lst)) wrld)
                     :controller-alist))
            (induct-vars1 (cdr lst) wrld)))))

(defun induct-vars (cand wrld)

; Historical Plaque from Nqthm:

;   Get all skos occupying controller slots in any of the terms associated
;   with this candidate.

; The age of that comment is not known, but the fact that we referred
; to the variables as "skos" (Skolem constants) suggests that it may
; date from the Interlisp version.  Meta comment: Perhaps someday some
; enterprising PhD student (in History?) will invent Software
; Archeology, in which decrepit fragments of archive tapes are pieced
; together and scrutinized for clues as to the way people thought back
; in the early days.

  (induct-vars1 (cons (access candidate cand :induction-term)
                      (access candidate cand :other-terms))
                wrld))

(defun vetoedp (cand vars lst changed-vars-flg)

; Vars is a list of variables.  We return t iff there exists a candidate
; in lst, other than cand, whose unchangeable-vars (or, if changed-vars-flg,
; changed-vars or unchangeable-vars) intersect with vars.

; This function is used both by compute-vetoes1, where flg is t and
; vars is the list of changing induction vars of cand, and by
; compute-vetoes2, where flg is nil and vars is the list of
; changed-vars cand.  We combine these two into one function simply to
; eliminate a definition from the system.

  (cond ((null lst) nil)
        ((equal cand (car lst))
         (vetoedp cand vars (cdr lst) changed-vars-flg))
        ((and changed-vars-flg
              (intersectp-eq vars
                             (access candidate (car lst) :changed-vars)))
         t)
        ((intersectp-eq vars
                        (access candidate (car lst) :unchangeable-vars))
         t)
        (t (vetoedp cand vars (cdr lst) changed-vars-flg))))

(defun compute-vetoes1 (lst cand-lst wrld)

; Lst is a tail of cand-lst.  We throw out from lst any candidate
; whose changing induct-vars intersect the changing or unchanging vars
; of another candidate in cand-lst.  We assume no two elements of
; cand-lst are equal, an invariant assured by the fact that we have
; done merging and flushing before this.

  (cond ((null lst) nil)
        ((vetoedp (car lst)
                  (intersection-eq
                   (access candidate (car lst) :changed-vars)
                   (induct-vars (car lst) wrld))
                  cand-lst
                  t)
         (compute-vetoes1 (cdr lst) cand-lst wrld))
        (t (cons (car lst)
                 (compute-vetoes1 (cdr lst) cand-lst wrld)))))

; If the first veto computation throws out all candidates, we revert to
; another heuristic.

(defun compute-vetoes2 (lst cand-lst)

; Lst is a tail of cand-lst.  We throw out from lst any candidate
; whose changed-vars intersect the unchangeable-vars of another
; candidate in cand-lst.  Again, we assume no two elements of cand-lst
; are equal.

  (cond ((null lst) nil)
        ((vetoedp (car lst)
                  (access candidate (car lst) :changed-vars)
                  cand-lst
                  nil)
         (compute-vetoes2 (cdr lst) cand-lst))
        (t (cons (car lst)
                 (compute-vetoes2 (cdr lst) cand-lst)))))

(defun compute-vetoes (cand-lst wrld)

; We try two different techniques for throwing out candidates.  If the
; first throws out everything, we try the second.  If the second throws
; out everything, we throw out nothing.

; The two are: (1) throw out a candidate if its changing induct-vars
; (the variables in control slots that change) intersect with either
; the changed-vars or the unchangeable-vars of another candidate.  (2)
; throw out a candidate if its changed-vars intersect the
; unchangeable-vars of another candidate.

; Historical Plaque from Nqthm:

;   This function weeds out "unclean" induction candidates.  The
;   intuition behind the notion "clean" is that an induction is clean
;   if nobody is competing with it for instantiation of its variables.
;   What we actually do is throw out any candidate whose changing
;   induction variables -- that is the induction variables as computed
;   by induct-vars intersected with the changed vars of candidate --
;   intersect the changed or unchanged variables of another candidate.
;   The reason we do not care about the first candidates unchanging
;   vars is as follows.  The reason you want a candidate clean is so
;   that the terms riding on that cand will reoccur in both the
;   hypothesis and conclusion of an induction.  There are two ways to
;   assure (or at least make likely) this: change the variables in the
;   terms as specified or leave them constant.  Thus, if the first
;   cand's changing vars are clean but its unchanging vars intersect
;   another cand it means that the first cand is keeping those other
;   terms constant, which is fine. (Note that the first cand would be
;   clean here.  The second might be clean or dirty depending on
;   whether its changed vars or unchanged vars intersected the first
;   cand's vars.)  The reason we check only the induction vars and not
;   all of the changed vars is if cand1's changed vars include some
;   induction vars and some accumulators and the accumulators are
;   claimed by another cand2 we believe that cand1 is still clean.
;   The motivating example was

;   (IMPLIES (MEMBER A C) (MEMBER A (UNION1 B C)))

;   where the induction on C is dirty because the induction on B and C
;   claims C, but the induction on B and C is clean because the B does
;   not occur in the C induction.  We do not even bother to check the
;   C from the (B C) induction because since it is necessarily an
;   accumulator it is probably being constructed and thus, if it
;   occurs in somebody else's ind vars it is probably being eaten so
;   it will be ok.  In formulating this heuristic we did not consider
;   the possibility that the accums of one candidate occur as
;   constants in the other.  Oh well.

;   July 20, 1978.  We have added an additional heuristic, to be
;   applied if the above one eliminates all cands.  We consider a cand
;   flawed if it changes anyone else's constants.  The motivating
;   example was GREATEST-FACTOR-LESSP -- which was previously proved
;   only by virtue of a very ugly use of the no-op fn ID to make a
;   certain induction flawed.

  (or (compute-vetoes1 cand-lst cand-lst wrld)
      (compute-vetoes2 cand-lst cand-lst)
      cand-lst))

; The next heuristic is to select complicated candidates, based on
; support for non-primitive recursive function schemas.

(defun induction-complexity1 (lst wrld)

; The "function" induction-complexity does not exist.  It is a symbol
; passed to maximal-elements-apply which calls this function on the list
; of terms supported by an induction candidate.  We count the number of
; non pr fns supported.

  (cond ((null lst) 0)
        ((getprop (ffn-symb (car lst)) 'primitive-recursive-defunp nil
                  'current-acl2-world wrld)
         (induction-complexity1 (cdr lst) wrld))
        (t (1+ (induction-complexity1 (cdr lst) wrld)))))

; We develop a general-purpose function for selecting maximal elements from
; a list under a measure.  That function, maximal-elements, is then used
; with the induction-complexity measure to collect both the most complex
; inductions and then to select those with the highest scores.

(defun maximal-elements-apply (fn x wrld)

; This function must produce an integerp.  This is just the apply function
; for maximal-elements.

  (case fn
        (induction-complexity
         (induction-complexity1 (cons (access candidate x :induction-term)
                                      (access candidate x :other-terms))
                                wrld))
        (score (access candidate x :score))
        (otherwise 0)))

(defun maximal-elements1 (lst winners maximum fn wrld)

; We are scanning down lst collecting into winners all those elements
; with maximal scores as computed by fn.  Maximum is the maximal score seen
; so far and winners is the list of all the elements passed so far with
; that score.

  (cond ((null lst) winners)
        (t (let ((temp (maximal-elements-apply fn (car lst) wrld)))
             (cond ((> temp maximum)
                    (maximal-elements1 (cdr lst)
                                       (list (car lst))
                                       temp fn wrld))
; PETE
; In other versions the = below is, mistakenly, an int=!                   

                   ((= temp maximum)
                    (maximal-elements1 (cdr lst)
                                       (cons (car lst) winners)
                                       maximum fn wrld))
                   (t
                    (maximal-elements1 (cdr lst)
                                       winners
                                       maximum fn wrld)))))))

(defun maximal-elements (lst fn wrld)

; Return the subset of lst that have the highest score as computed by
; fn.  The functional parameter fn must be known to maximal-elements-apply.
; We reverse the accumulated elements to preserve the order used by
; nqthm.

  (cond ((null lst) nil)
        ((null (cdr lst)) lst)
        (t (reverse
            (maximal-elements1 (cdr lst)
                               (list (car lst))
                               (maximal-elements-apply fn (car lst) wrld)
                               fn wrld)))))


; All that is left in the heuristic selection of the induction candidate is
; the function m&m that mates and merges arbitrary objects.  We develop that
; now.

; The following three functions are not part of induction but are
; used by other callers of m&m and so have to be introduced now
; so we can define m&m-apply and get on with induct.

(defun intersectp-eq/union-equal (x y)
  (cond ((intersectp-eq (car x) (car y))
         (cons (union-eq (car x) (car y))
               (union-equal (cdr x) (cdr y))))
        (t nil)))

(defun equal/union-equal (x y)
  (cond ((equal (car x) (car y))
         (cons (car x)
               (union-equal (cdr x) (cdr y))))
        (t nil)))

(defun subsetp-equal/smaller (x y)
  (cond ((subsetp-equal x y) x)
        ((subsetp-equal y x) y)
        (t nil)))

(defun m&m-apply (fn x y)

; This is a first-order function that really just applies fn to x and
; y, but does so only for a fixed set of fns.  In fact, this function
; handles exactly those functions that we give to m&m.

  (case fn
        (intersectp-eq/union-equal (intersectp-eq/union-equal x y))
        (equal/union-equal (equal/union-equal x y))
        (flush-candidates (flush-candidates x y))
        (merge-candidates (merge-candidates x y))
        (subsetp-equal/smaller (subsetp-equal/smaller x y))))

(defun count-off (n lst)

; Pair the elements of lst with successive integers starting at n.

  (cond ((null lst) nil)
        (t (cons (cons n (car lst))
                 (count-off (1+ n) (cdr lst))))))

(defun m&m-search (x y-lst del fn)

; Y-lst is a list of pairs, (id . y).  The ids are integers.  If id is
; a member of del, we think of y as "deleted" from y-lst.  That is,
; y-lst and del together characterize a list of precisely those y such
; that (id . y) is in y-lst and id is not in del.

; We search y-lst for the first y that is not deleted and that mates
; with x.  We return two values, the merge of x and y and the integer
; id of y.  If no such y exists, return two nils.

  (cond ((null y-lst) (mv nil nil))
        ((member (caar y-lst) del)
         (m&m-search x (cdr y-lst) del fn))
        (t (let ((z (m&m-apply fn x (cdar y-lst))))
             (cond (z (mv z (caar y-lst)))
                   (t (m&m-search x (cdr y-lst) del fn)))))))

(defun m&m1 (pairs del ans n fn)

; This is workhorse for m&m.  See that fn for a general description of
; the problem and the terminology.  Pairs is a list of pairs.  The car
; of each pair is an integer and the cdr is a possible element of the
; bag we are closing under fn.  Del is a list of the integers
; identifying all the elements of pairs that have already been
; deleted.  Abstractly, pairs and del together represent a bag we call
; the "unprocessed bag".  The elements of the unprocessed bag are
; precisely those ele such that (i . ele) is in pairs and i is not in
; del.

; Without assuming any properties of fn, this function can be
; specified as follows: If the first element, x, of the unprocessed
; bag, mates with some y in the rest of the uprocessed bag, then put
; the merge of x and the first such y in place of x, delete that y,
; and iterate.  If the first element has no such mate, put it in the
; answer accumulator ans.  N, by the way, is the next available unique
; identifier integer.

; If one is willing to make the assumptions that the mate and merge
; fns of fn are associative and commutative and have the distributive
; and non-preclusion properties, then it is possible to say more about
; this function.  The rest of this comment makes those assumptions.

; Ans is a bag with the property that no element of ans mates with any
; other element of ans or with any element of the unprocessed bag.  N
; is the next available unique identifier integer; it is always larger
; than any such integer in pairs or in del.

; Abstractly, this function closes B under fn, where B is the bag
; union of the unprocessed bag and ans.

  (cond
   ((null pairs) ans)
   ((member (caar pairs) del)
    (m&m1 (cdr pairs) del ans n fn))
   (t (mv-let (mrg y-id)
        (m&m-search (cdar pairs) (cdr pairs) del fn)
        (cond
         ((null mrg)
          (m&m1 (cdr pairs)
                del
                (cons (cdar pairs) ans)
                n fn))
         (t (m&m1 (cons (cons n mrg) (cdr pairs))
                  (cons y-id del)
                  ans
                  (1+ n)
                  fn)))))))

(defun m&m (bag fn)

; This function takes a bag and a symbol naming a dyadic function, fn,
; known to m&m-apply and about which we assume certain properties
; described below.  Let z be (m&m-apply fn x y).  Then we say x and y
; "mate" if z is non-nil.  If x and y mate, we say z is the "merge" of
; x and y.  The name of this function abbreviates the phrase "mate and
; merge".

; We consider each element, x, of bag in turn and seek the first
; successive element, y, that mates with it.  If we find one, we throw
; out both, add their merge in place of x and iterate.  If we find no
; mate for x, we deposit it in our answer accumulator.

; The specification above is explicit about the order in which we try
; the elements of the bag.  If we try to loosen the specification so
; that order is unimportant, we must require that fn have certain
; properties.  We discuss this below.

; First, note that we have implicitly assumed that mate and merge are
; commutative because we haven't said in which order we present the
; arguments.

; Second, note that if x doesn't mate with any y, we set it aside in
; our accumulating answer.  We do not even try to mate such an x with
; the offspring of the y's it didn't like.  This makes us order
; dependent.  For example, consider the bag {x y1 y2}.  Suppose x
; won't mate with either y1 or y2, but that y1 mates with y2 to
; produce y3 and x mates with y3 to produce y4.  Then if we seek mates
; for x first we find none and it gets into our final answer.  Then y1
; and y2 mate to form y3.  The final answer is hence {x y3}.  But if
; we seek mates for y1 first we find y2, produce y3, add it to the
; bag, forming {y3 x}, and then mate x with y3 to get the final answer
; {y4}.  This order dependency cannot arise if fn has the property
; that if x mates with the merge of y and z then x mates with either y
; or z.  This is called the "distributive" property of mate over merge.

; Third, note that if x does mate with y to produce z then we throw x
; out in favor of z.  Thus, x is not mated against any but the first
; y.  Thus, if we have {x y1 y2} and x mates with y1 to form z1 and x
; mates with y2 to form z2 and there are no other mates, then we can
; either get {z1 y2} or {z2 y1} as the final bag, depending on whether
; we mate x with y1 or y2.  This order dependency cannot arise if fn
; has the property that if x mates with y1 and x mates with y2, then
; (a) the merge of x and y1 mates with y2, and (b) merge has the
; "commutativity-2" (merge (merge x y1) y2) = (merge (merge x y2) y1).
; We call property (a) "non-preclusion" property of mate and merge,
; i.e., merging doesn't preclude mating.

; The commutativity-2 property is implied by associativity and (the
; already assumed commutativity).  Thus, another way to avoid the
; third order dependency is if legal merges are associative and have
; the non-preclusion property.

; Important Note: The commonly used fn of unioning together two alists
; that agree on the intersection of their domains, does not have the
; non-preclusion property!  Suppose x, y1, and y2 are all alists and
; all map A to 0.  Suppose in addition y1 maps B to 1 but y2 maps B to
; 2.  Finally, suppose x maps C to 3.  Then x mates with both y1 and
; y2.  But merging y1 into x precludes mating with y2 and vice versa.

; We claim, but do not prove, that if the mate and merge functions for
; fn are commutative and associative, and have the distributive and
; non-preclusion properties, then m&m is order independent.

; For efficiency we have chosen to implement deletion by keeping a
; list of the deleted elements.  But we cannot make a list of the
; deleted elements themselves because there may be duplicate elements
; in the bag and we need to be able to delete occurrences.  Thus, the
; workhorse function actually operates on a list of pairs, (i . ele),
; where i is a unique identification integer and ele is an element of
; the bag.  In fact we just assign the position of each occurrence to
; each element of the initial bag and thereafter count up as we
; generate new elements.
;
; See m&m1 for the details.

  (m&m1 (count-off 0 bag) nil nil (length bag) fn))

; We now develop a much more powerful concept, that of mapping m&m over the
; powerset of a set.  This is how we actually merge induction candidates.
; That is, we try to mash together every possible subset of the candidates,
; largest subsets first.  See m&m-over-powerset for some implementation
; commentary before going on.

(defun cons-subset-tree (x y)

; We are representing full binary trees of t's and nil's and
; collapsing trees of all nil's to nil and trees of all t's to t.  See
; the long comment in m&m-over-powerset.  We avoid consing when
; convenient.

  (if (eq x t)
      (if (eq y t)
          t
        (if y (cons x y) '(t)))
    (if x
        (cons x y)
      (if (eq y t)
          '(nil . t)
        (if y (cons x y) nil)))))

(defabbrev car-subset-tree (x)

; See cons-subset-tree.

  (if (eq x t) t (car x)))

(defabbrev cdr-subset-tree (x)

; See cons-subset-tree.

  (if (eq x t) t (cdr x)))

(defun or-subset-trees (tree1 tree2)

; We disjoin the tips of two binary t/nil trees.  See cons-subset-tree.

  (cond ((or (eq tree1 t)(eq tree2 t)) t)
        ((null tree1) tree2)
        ((null tree2) tree1)
        (t (cons-subset-tree (or-subset-trees (car-subset-tree tree1)
                                              (car-subset-tree tree2))
                             (or-subset-trees (cdr-subset-tree tree1)
                                              (cdr-subset-tree tree2))))))

(defun m&m-over-powerset1 (st subset stree ans fn)

; See m&m-over-powerset.

  (cond
   ((eq stree t) (mv t ans))
   ((null st)
    (let ((z (m&m subset fn)))
      (cond ((and z (null (cdr z)))
             (mv t (cons (car z) ans)))
            (t (mv nil ans)))))
   (t
    (mv-let (stree1 ans1)
      (m&m-over-powerset1 (cdr st)
                          (cons (car st) subset)
                          (cdr-subset-tree stree)
                          ans fn)
      (mv-let (stree2 ans2)
        (m&m-over-powerset1 (cdr st)
                            subset
                            (or-subset-trees
                             (car-subset-tree stree)
                             stree1)
                            ans1 fn)
        (mv (cons-subset-tree stree2 stree1) ans2))))))

(defun m&m-over-powerset (st fn)

; Fn is a function known to m&m-apply.  Let (fn* s) be defined to be z,
; if (m&m s fn) = {z} and nil otherwise.  Informally, (fn* s) is the
; result of somehow mating and merging all the elements of s into a single
; object, or nil if you can't.

; This function applies fn* to the powerset of st and collects all those
; non-nil values produced from maximal s's.  I.e., we keep (fn* s) iff it
; is non-nil and no superset of s produces a non-nil value.

; We do this amazing feat (recall that the powerset of a set of n
; things contains 2**n subsets) by generating the powerset in order
; from largest to smallest subsets and don't generate or test any
; subset under a non-nil fn*.  Nevertheless, if the size of set is
; very big, this function will get you.

; An informal specification of this function is that it is like m&m
; except that we permit an element to be merged into more than one
; other element (but an element can be used at most once per final
; element) and we try to maximize the amount of merging we can do.

; For example, if x mates with y1 to form z1, and x mates with y2 to
; form z2, and no other mates occur, then this function would
; transform {x y1 y2} into {z1 z2}.  It searches by generate and test:

;       s            (fn* s)
;    (x y1 y2)         nil
;    (x y1)            z1
;    (x y2)            z2
;    (x)              subsumed
;    (y1 y2)           nil
;    (y1)             subsumed
;    (y2)             subsumed
;    nil              subsumed

; Here, s1 is "subsumed" by s2 means s1 is a subset of s2.  (Just the
; opposite technical definition but exactly the same meaning as in the
; clausal sense.)

; The way we generate the powerset elements is suggested by the
; following trivial von Neumann function, ps, which, when called as in
; (ps set nil), calls PROCESS on each member of the powerset of set,
; in the order in which we generate them:

; (defun ps (set subset)
;  (cond ((null set) (PROCESS subset))
;        (t (ps (cdr set) (cons (car set) subset))   ;rhs
;           (ps (cdr set) subset))))                 ;lhs

; By generating larger subsets first we know that if a subset subsumes
; the set we are considering then that subset has already been
; considered.  Therefore, we need a way to keep track of the subsets
; with non-nil values.  We do this with a "subset tree".  Let U be the
; universe of objects in some order.  Then the full binary tree with
; depth |U| can be thought of as the powerset of U.  In particular,
; any branch through the tree, from top-most node to tip, represents a
; subset of U by labelling the nodes at successive depth by the
; successive elements of U (the topmost node being labelled with the
; first element of U) and adopting the convention that taking a
; right-hand (cdr) branch at a node indicates that the label is in the
; subset and a left-hand (car) branch indicates that the label is not
; in the subset.  At the tip of the tree we store a T indicating that
; the subset had a non-nil value or a NIL indicating that it had a nil
; value.

; For storage efficiency we let nil represent an arbitrarily deep full
; binary tree will nil at every tip and we let t represent the
; analogous trees with t at every tip.  Car-subset-tree,
; cdr-subset-tree and cons-subset-tree implement these abstractions.

; Of course, we don't have the tree when we start and we generate it
; as we go.  That is a really weird idea because generating the tree
; that tells us who was a subset of whom in the past seems to have little
; use as we move forward.  But that is not true.

; Observe that there is a correspondence between these trees and the
; function ps above for generating the power set.  The recursion
; labelled "rhs" above is going down the right-hand side of the tree
; and the "lhs" recursion is going down the left-hand side.  Note that
; we go down the rhs first.

; The neat fact about these trees is that there is a close
; relationship between the right-hand subtree (rhs) and left-hand
; subtree (lhs) of any given node of the tree: lhs can be obtained
; from rhs by turning some nils into ts.  The reason is that the tips
; of the lhs of a node labelled by x denote exactly the same subsets
; as the corresponding tips of the right-hand side, except that on the
; right x was present in the subset and on the left it is not.  So
; when we do the right hand side we come back with a tree and if we
; used that very tree for the left hand side (interpreting nil as
; meaning "compute it and see" and t as meaning "a superset of this
; set has non-nil value") then it is correct.  But we can do a little
; better than that because we might have come into this node with a
; tree (i.e., one to go into the right hand side with and another to go
; into the left hand side with) and so after we have gone into the
; right and come back with its new tree, we can disjoin the output of
; the right side with the input for the left side to form the tree we
; will actually use to explore the left side.

  (mv-let (stree ans)
    (m&m-over-powerset1 st nil nil nil fn)
    (declare (ignore stree))
    ans))

; Ok, so now we have finished the selection process and we begin the
; construction of the induction formula itself.


(defun all-picks2 (pocket pick ans)
; See all-picks.
  (cond ((null pocket) ans)
        (t (cons (cons (car pocket) pick)
                 (all-picks2 (cdr pocket) pick ans)))))

(defun all-picks2r (pocket pick ans)
; See all-picks.
  (cond ((null pocket) ans)
        (t (all-picks2r (cdr pocket) pick
                        (cons (cons (car pocket) pick) ans)))))

(defun all-picks1 (pocket picks ans rflg)
; See all-picks.
  (cond ((null picks) ans)
        (t (all-picks1 pocket (cdr picks)
                       (if rflg
                           (all-picks2r pocket (car picks) ans)
                         (all-picks2 pocket (car picks) ans))
                       rflg))))

(defun all-picks (pockets rflg)

; Pockets is a list of pockets, each pocket containing 0 or more
; objects.  We return a list of all the possible ways you can pick one
; thing from each pocket.  If rflg is nil initially, then the order of
; the resulting list is exactly the same as it was in nqthm.  There is
; not much else to recommend this particular choice of definition!

; Historical Plaque from Nqthm:

;   (DEFUN ALL-PICKS (POCKET-LIST)
;    (COND ((NULL POCKET-LIST) (LIST NIL))
;          (T (ITERATE FOR PICK IN (ALL-PICKS (CDR POCKET-LIST))
;                      NCONC (ITERATE FOR CHOICE IN (CAR POCKET-LIST)
;                                     COLLECT (CONS CHOICE PICK))))))

; Nqthm's construction is a very natural recursive one, except that it
; used nconc to join together the various segments of the answer.  If
; we tried the analogous construction here we would have to append the
; segments together and copy a very long list.  So we do it via an
; accumulator.  The trouble however is that we reverse the order of
; the little buckets in our answer every time we process a pocket.  We
; could avoid that if we wanted to recurse down the length of our
; answer on recursive calls, but we were afraid of running out of
; stack, and so we have coded this with tail recursion only.  We do
; non-tail recursion only over short things like individual pockets or
; the list of pockets.  And so to (a) avoid unnecessary copying, (b)
; non-tail recursion, and (c) constructing our answer in a different
; order, we introduced rflg.  Rflg causes us either to reverse or not
; reverse a certain intermediate result every other recursion.  It
; would be reassuring to see a mechanically checked proof that this
; definition of all-picks is equivalent to nqthm's.

  (cond ((null pockets) '(nil))
        (t (all-picks1 (car pockets)
                       (all-picks (cdr pockets) (not rflg))
                       nil
                       rflg))))



(defun dumb-negate-lit-lst-lst (cl-set)

; We apply dumb-negate-lit-lst to every list in cl-set and collect the
; result.  You can think of this as negating a clause set (i.e., an
; implicit conjunction of disjunctions), but you have to then imagine
; that the implicit "and" at the top has been turned into an "or" and
; vice versa at the lower level.

  (cond ((null cl-set) nil)
        (t (cons (dumb-negate-lit-lst (car cl-set))
                 (dumb-negate-lit-lst-lst (cdr cl-set))))))

(defun induction-hyp-clause-segments2 (alists cl ans)
; See induction-hyp-clause-segments1.
  (cond ((null alists) ans)
        (t (cons (sublis-var-lst (car alists) cl)
                 (induction-hyp-clause-segments2 (cdr alists) cl ans)))))

(defun induction-hyp-clause-segments1 (alists cl-set ans)

; This function applies all of the substitutions in alists to all of
; the clauses in cl-set and appends the result to ans to create one
; list of instantiated clauses.

  (cond ((null cl-set) ans)
        (t (induction-hyp-clause-segments2
            alists
            (car cl-set)
            (induction-hyp-clause-segments1 alists (cdr cl-set) ans)))))

(defun induction-hyp-clause-segments (alists cl-set)

; Cl-set is a set of clauses.  We are trying to prove the conjunction
; over that set, i.e., cl1 & cl2 ... & clk, by induction.  We are in a
; case in which we can assume every instance under alists of that
; conjunction.  Thus, we can assume any lit from cl1, any lit from
; cl2, etc., instantiated via all of the alists.  We wish to return a
; list of clause segments.  Each segment will be spliced into the a
; clause we are trying to prove and together the resulting set of
; clauses is supposed to be equivalent to assuming all instances of
; the conjunction over cl-set.

; So one way to create the answer would be to first instantiate each
; of the k clauses with each of the n alists, getting a set of n*k
; clauses.  Then we could run all-picks over that, selecting one
; literal from each of the instantiated clauses to assume.  Then we'd
; negate each literal within each pick to create a clause hypothesis
; segment.  That is nearly what we do, except that we do the negation
; first so as to share structure among the all-picks answers.


; Note: The code below calls (dumb-negate-lit lit) on each lit.  Nqthm
; used (negate-lit lit nil ...) on each lit, employing
; negate-lit-lst-lst, which has since been deleted but was strictly
; analogous to the dumb version called below.  But since the
; type-alist is nil in Nqthm's call, it seems unlikely that the
; literal will be decided by type-set.  We changed to dumb-negate-lit
; to avoid having to deal both with ttrees and the enabled structure
; implicit in type-set.

  (all-picks
   (induction-hyp-clause-segments1 alists
                                   (dumb-negate-lit-lst-lst cl-set)
                                   nil)
   nil))

(defun induction-formula3 (neg-tests hyp-segments cl ans)

; Neg-tests is the list of the negated tests of an induction
; tests-and-alists entry.  hyp-segments is a list of hypothesis clause
; segments (i.e., more negated tests), and cl is a clause.  For each
; hyp segment we create the clause obtained by disjoining the tests,
; the segment, and cl.  We conjoin the resulting clauses to ans.

; See induction-formula for a comment about this iteration.

  (cond
   ((null hyp-segments) ans)
   (t (induction-formula3 neg-tests
                          (cdr hyp-segments)
                          cl
                          (conjoin-clause-to-clause-set

; Historical Plaque from Nqthm:

;   We once implemented the idea of "homographication" in which we combined
;   both induction, opening up of the recursive fns in the conclusion, and
;   generalizing away some recursive calls.  This function did the expansion
;   and generalization.  If the idea is reconsidered the following theorems are
;   worthy of consideration:

;       (ORDERED (SORT X)),
;       (IMPLIES (ORDERED X)
;                (ORDERED (ADDTOLIST I X))),
;       (IMPLIES (AND (NUMBER-LISTP X)
;                     (ORDERED X)
;                     (NUMBERP I)
;                     (NOT (< (CAR X) I)))
;                (EQUAL (ADDTOLIST I X) (CONS I X))), and
;       (IMPLIES (AND (NUMBER-LISTP X) (ORDERED X)) (EQUAL (SORT X) X)).

; Observe that we simply disjoin the negated tests, hyp segments, and clause.
; Homographication further manipulated the clause before adding it to the
; answer.
                           (disjoin-clauses
                            neg-tests
                            (disjoin-clauses (car hyp-segments) cl))
                           ans)))))

(defun induction-formula2 (cl cl-set ta-lst ans)

; Cl is a clause in cl-set, which is a set of clauses we are proving
; by induction.  Ta-lst is the tests-and-alists-lst component of the
; induction candidate we are applying to prove cl-set.  We are now
; focussed on the proof of cl, using the induction schema of ta-lst
; but getting to assume all the clauses in cl-set in our induction
; hypothesis.  We will map across ta-lst, getting a set of tests and
; some alists at each stop, and for each stop add a bunch of clauses
; to ans.

  (cond
   ((null ta-lst) ans)
   (t (induction-formula2 cl cl-set (cdr ta-lst)
                          (induction-formula3

; Note:  Nqthm used (negate-lit-lst ... nil ...), but since the
; type-alist supplied was nil, we decided it was probably no buying us
; much -- not as much as passing up the ttrees would cost in terms of
; coding work!

                           (dumb-negate-lit-lst
                            (access tests-and-alists (car ta-lst) :tests))
                           (induction-hyp-clause-segments
                            (access tests-and-alists (car ta-lst) :alists)
                            cl-set)
                           cl
                           ans)))))

(defun induction-formula1 (lst cl-set ta-lst ans)

; Lst is a tail of cl-set.  Cl-set is a set of clauses we are trying to prove.
; Ta-lst is the tests-and-alists-lst component of the induction candidate
; we wish to apply to cl-set.  We map down lst forming a set of clauses
; for each cl in lst.  Basically, the set we form for cl is of the form
; ... -> cl, where ... involves all the case analysis under the tests in
; ta-lst and all the induction hypotheses from cl-set under the alists in
; each test-and-alists.  We add our clauses to ans.

  (cond
   ((null lst) ans)
   (t (induction-formula1 (cdr lst) cl-set ta-lst
                          (induction-formula2 (car lst)
                                              cl-set ta-lst ans)))))

(defun induction-formula (cl-set ta-lst)

; Cl-set is a set of clauses we are to try to prove by induction, applying
; the inductive scheme described by the tests-and-alists-lst, ta-lst,
; of some induction candidate.  The following historical plaque tells all.

; Historical Plaque from Nqthm:

;   TESTS-AND-ALISTS-LST is a such a list that the disjunction of the
;   conjunctions of the TESTS components of the members is T.  Furthermore,
;   there exists a measure M, a well-founded relation R, and a sequence of
;   variables x1, ..., xn such that for each T&Ai in TESTS-AND-ALISTS-LST, for
;   each alist alst in the ALISTS component of T&Ai, the conjunction of the
;   TESTS component, say qi, implies that (R (M x1 ... xn)/alst (M x1 ... xn)).

;   To prove thm, the conjunction of the disjunctions of the members of CL-SET,
;   it is sufficient, by the principle of induction, to prove instead the
;   conjunction of the terms qi & thm' & thm'' ...  -> thm, where the primed
;   terms are the results of substituting the alists in the ALISTS field of the
;   ith member of TESTS-AND-ALISTS-LST into thm.

;   If thm1, thm2, ..., thmn are the disjunctions of the members of CL-SET,
;   then it is sufficient to prove all of the formulas qi & thm' & thm'' ...
;   -> thmj.  This is a trivial proposition fact, to prove (IMPLIES A (AND B
;   C)) it is sufficient to prove (IMPLIES A B) and (IMPLIES A C).

;   The (ITERATE FOR PICK ...)* expression below returns a list of
;   clauses whose conjunction propositionally implies qi & thm' &
;   thm'' ...  -> thmj, where TA is the ith member of
;   TESTS-AND-ALISTS-LST and CL is the jth member of CL-SET.  Proof:
;   Let THM have the form:
;
;        (AND (OR a1 ...)
;             (OR b1 ...)
;             ...
;             (OR z1 ...)).

;   Then qi & thm' & thm'' ... -> thmj has the form:

;       (IMPLIES (AND qi
;                     (AND (OR a1 ... )
;                          (OR b1 ... )
;                          ...
;                          (OR z1 ... ))'
;                     (AND (OR a1 ... )
;                          (OR b1 ... )
;                          ...
;                          (OR z1 ... ))''
;                     ...
;                     (AND (OR a1 ... )
;                          (OR b1 ... )
;                          ...
;                          (OR z1 ... )))'''...'
;                thmj).
;
;   Suppose this formula is false for some values of the free variables.  Then
;   under those values, each disjunction in the hypothesis is true.  Thus there
;   exists a way of choosing one literal from each of the disjunctions, all of
;   which are true.  This choice is one of the PICKs below.  But we prove that
;   (IMPLIES (AND qi PICK) thmj).

; Note: The (ITERATE FOR PICK ...) expression mentioned above is the function
; induction-formula3 above.

  (m&m (reverse (induction-formula1 cl-set cl-set ta-lst nil))
       'subsetp-equal/smaller))

; Because the preceding computation is potentially explosive we will
; sometimes reduce its complexity by shrinking the given clause set to
; a singleton set containing a unit clause.  To decide whether to do that
; we will use the following rough measures:

(defun all-picks-size (cl-set)

; This returns the size of the all-picks computed by induction-formula3.

  (cond ((null cl-set) 1)
        (t (* (length (car cl-set)) (all-picks-size (cdr cl-set))))))

(defun induction-formula-size1 (hyps-size concl-size ta-lst)

; We determine roughly the number of clauses that ta-lst will generate when
; the number of all-picks through the hypotheses is hyps-size and the
; number of conclusion clauses is concl-size.  The individual cases of
; the tests-and-alists combine additively.  But we must pick our way through
; the hyps for each instantiation.

  (cond ((null ta-lst) 0)
        (t
         (+ (* concl-size (expt hyps-size
                                (length (access tests-and-alists
                                                (car ta-lst)
                                                :alists))))
            (induction-formula-size1 hyps-size concl-size (cdr ta-lst))))))

(defun induction-formula-size (cl-set ta-lst)

; This function returns a rough upper bound on the number of clauses
; that will be generated by induction-formula on the given arguments.
; See the comment in that function.

  (induction-formula-size1 (all-picks-size cl-set)
                           (length cl-set)
                           ta-lst))

; The following constant determines the limit on the estimated number of
; clauses induct, below, will return.  When normal processing would exceed
; this number, we try to cut down the combinatorics by collapsing clauses
; back into terms.

(defconst *maximum-induct-size* 100)

; And here is how we convert a hairy set of clauses into a term when we
; have to.

(defun termify-clause-set (clauses)

; This function is similar to termify-clause except that it converts a
; set of clauses into an equivalent term.  The set of clauses is
; understood to be implicitly conjoined and we therefore produce a
; conjunction expressed as (if cl1 cl2 nil).

  (cond ((null clauses) *t*)
        ((null (cdr clauses)) (disjoin (car clauses)))
        (t (mcons-term* 'if
                        (disjoin (car clauses))
                        (termify-clause-set (cdr clauses))
                        *nil*))))

; Once we have created the set of clauses to prove, we inform the
; simplifier of what to look out for during the early processing.

(defun inform-simplify3 (alist terms ans)

; Instantiate every term in terms with alist and add them to ans.

  (cond ((null terms) ans)
        (t (inform-simplify3 alist (cdr terms)
                             (add-to-set-equal (sublis-var alist (car terms))
                                               ans)))))

(defun inform-simplify2 (alists terms ans)

; Using every alist in alists, instantiate every term in terms and add
; them all to ans.

  (cond ((null alists) ans)
        (t (inform-simplify2 (cdr alists) terms
                             (inform-simplify3 (car alists) terms ans)))))


(defun inform-simplify1 (ta-lst terms ans)

; Using every alist mentioned in any tests-and-alists record of ta-lst
; we instantiate every term in terms and add them all to ans.

  (cond ((null ta-lst) ans)
        (t (inform-simplify1 (cdr ta-lst) terms
                             (inform-simplify2 (access tests-and-alists
                                                       (car ta-lst)
                                                       :alists)
                                               terms
                                               ans)))))


(defun inform-simplify (ta-lst terms pspv)

; Historical Plaque from Nqthm:

;   Two of the variables effecting REWRITE are TERMS-TO-BE-IGNORED-BY-REWRITE
;   and EXPAND-LST.  When any term on the former is encountered REWRITE returns
;   it without rewriting it.  Terms on the latter must be calls of defined fns
;   and when encountered are replaced by the rewritten body.

;   We believe that the theorem prover will perform significantly faster on
;   many theorems if, after an induction, it does not waste time (a) trying to
;   simplify the recursive calls introduced in the induction hypotheses and (b)
;   trying to decide whether to expand the terms inducted for in the induction
;   conclusion.  This suspicion is due to some testing done with the idea of
;   "homographication" which was just a jokingly suggested name for the idea of
;   generalizing the recursive calls away at INDUCT time after expanding the
;   induction terms in the conclusion.  Homographication speeded the
;   theorem-prover on many theorems but lost on several others because of the
;   premature generalization.  See the comment in FORM-INDUCTION-CLAUSE.

;   To avoid the generalization at INDUCT time we are going to try using
;   TERMS-TO-BE-IGNORED-BY-REWRITE.  The idea is this, during the initial
;   simplification of a clause produced by INDUCT we will have the recursive
;   terms on TERMS-TO-BE-IGNORED-BY-REWRITE.  When the clause settles down --
;   hopefully it will often be proved first -- we will restore
;   TERMS-TO-BE-IGNORED-BY-REWRITE to its pre-INDUCT value.  Note however that
;   we have to mess with TERMS-TO-BE-IGNORED-BY-REWRITE on a clause by clause
;   basis, not just once in INDUCT.

;   So here is the plan.  INDUCT will set INDUCTION-HYP-TERMS to the list of
;   instances of the induction terms, and will set INDUCTION-CONCL-TERMS to the
;   induction terms themselves.  SIMPLIFY-CLAUSE will look at the history of
;   the clause to determine whether it has settled down since induction.  If
;   not it will bind TERMS-TO-BE-IGNORED-BY-REWRITE to the concatenation of
;   INDUCTION-HYP-TERMS and its old value and will analogously bind EXPAND-LST.
;   A new process, called SETTLED-DOWN-SENT, will be used to mark when in the
;   history the clause settled down.

; In a departure from Nqthm, starting with Version_2.8, we do not wait for
; settled-down before turning off the above special consideration given to
; induction-hyp-terms and induction-concl-terms. See simplify-clause for
; details.

  (change prove-spec-var pspv
          :induction-concl-terms terms
          :induction-hyp-terms (inform-simplify1 ta-lst terms nil)))

; Ok, except for our output and putting it all together, that's induction.
; We now turn to the output.  Induct prints two different messages. One
; reports the successful choice of an induction.  The other reports failure.

(defun all-vars1-lst-lst (lst ans)

; Lst is a list of lists of terms.  For example, it might be a set of
; clauses.  We compute the set of all variables occuring in it.

  (cond ((null lst) ans)
        (t (all-vars1-lst-lst (cdr lst)
                              (all-vars1-lst (car lst) ans)))))

(defun gen-new-name1 (char-lst wrld i)
  (let ((name (intern
               (coerce
                (append char-lst
                        (explode-nonnegative-integer i 10 nil))
                'string)
               "ACL2")))
    (cond ((new-namep name wrld) name)
          (t (gen-new-name1 char-lst wrld (1+ i))))))

(defun gen-new-name (root wrld)

; Create from the symbol root a possibly different symbol that
; is a new-namep in wrld.

  (cond ((new-namep root wrld) root)
        (t (gen-new-name1 (coerce (symbol-name root) 'list) wrld 0))))

(defun unmeasured-variables3 (vars alist)
; See unmeasured-variables.
  (cond ((null alist) nil)
        ((or (member-eq (caar alist) vars)
             (eq (caar alist) (cdar alist)))
         (unmeasured-variables3 vars (cdr alist)))
        (t (cons (caar alist) (unmeasured-variables3 vars (cdr alist))))))

(defun unmeasured-variables2 (vars alists)
; See unmeasured-variables.
  (cond ((null alists) nil)
        (t (union-eq (unmeasured-variables3 vars (car alists))
                     (unmeasured-variables2 vars (cdr alists))))))

(defun unmeasured-variables1 (vars ta-lst)
; See unmeasured-variables.
  (cond ((null ta-lst) nil)
        (t (union-eq (unmeasured-variables2 vars
                                            (access tests-and-alists
                                                    (car ta-lst)
                                                    :alists))
                     (unmeasured-variables1 vars (cdr ta-lst))))))

(defun unmeasured-variables (measured-vars cand)

; Measured-vars is the :subset of measured variables from the measure of term,
; computed above, for cand.  We collect those variables that are changed by
; some substitution but are not measured by our induction measure.  These are
; simply brought to the user's attention because we find it often surprising to
; see them.

  (unmeasured-variables1 measured-vars
                         (access candidate cand :tests-and-alists-lst)))

(defun tilde-@-well-founded-relation-phrase (rel wrld)

; We return a ~@ message that prints as "the relation rel (which, by name, is
; known to be well-founded on the domain recognized by mp)" and variants of
; that obtained when name is nil (meaning the well-foundedness is builtin)
; and/or mp is t (meaning the domain is the universe).

  (let* ((temp (assoc-eq rel (global-val 'well-founded-relation-alist wrld)))
         (mp (cadr temp))
         (base-symbol (base-symbol (cddr temp))))
    (msg "the relation ~x0 (which~#1~[ ~/, by ~x2, ~]is known to be ~
          well-founded~#3~[~/ on the domain recognized by ~x4~])"
         rel
         (if (null base-symbol) 0 1)
         base-symbol
         (if (eq mp t) 0 1)
         mp)))

(defun measured-variables (cand wrld)
  (all-vars1-lst
   (subcor-var-lst (formals (ffn-symb (access candidate cand :induction-term))
                            wrld)
                   (fargs (access candidate cand :induction-term))
                   (access justification
                           (access candidate cand :justification)
                           :subset))
   nil))

(defun induct-msg/continue (pool-name
                            cl-set
                            induct-hint-val
                            len-candidates
                            len-flushed-candidates
                            len-merged-candidates
                            len-unvetoed-candidates
                            len-complicated-candidates
                            len-high-scoring-candidates
                            winning-candidate
                            estimated-size
                            clauses
                            wrld
                            state)

; Pool-name is the tilde-@-pool-name-phrase (q.v.) of the set of
; clauses cl-set to which we are applying induction.  Len-candidates
; is the length of the list of induction candidates we found.
; Len-flushed-candidates is the length of the candidates after
; flushing some down others, etc.  Winning-candidate is the final
; selection.  Clauses is the clause set generated by applying
; winning-candidate to cl-set.  Wrld and state are the usual.

; This function increments timers.  Upon entry, the accumulated time is
; charged to 'prove-time.  The time spent in this function is charged
; to 'print-time.

; Warning: This function should be called under (io? prove ...).

  (pprogn
   (increment-timer 'prove-time state)
   (let* ((p (cons :p
                   (merge-sort-term-order (all-vars1-lst-lst cl-set nil))))
          (measured-variables (measured-variables winning-candidate wrld))
          (unmeasured-variables (unmeasured-variables measured-variables
                                                      winning-candidate))
          (attribution-phrase (tilde-*-simp-phrase
                               (access candidate winning-candidate :ttree))))
     (fms "~#H~[We have been told to use induction.  ~N0 induction ~
                scheme~#1~[ is~/s are~] suggested by the induction ~
                hint.~/~

                We have been told to use induction.  ~N0 induction ~
                scheme~#1~[ is~/s are~] suggested by this ~
                conjecture.~/~

                Perhaps we can prove ~@n by induction.  ~

                ~N0 induction scheme~#1~[ is~/s are~] suggested by this ~
                conjecture.~]  ~

          ~#a~[~/Subsumption reduces that number to ~n2.  ~]~

          ~#b~[~/These merge into ~n3 derived induction scheme~#4~[~/s~].  ~]~

          ~#c~[~/However, ~n5 of these ~#6~[is~/are~] flawed and so we are ~
           left with ~nq viable ~#r~[~/candidate~/candidates~].  ~]~

          ~#d~[~/By considering those suggested by the largest number of ~
                 non-primitive recursive functions, we narrow the field ~
                 to ~n7.  ~]~

          ~#e~[~/~N8 of these ~
                 ~#9~[has a score higher than the other~#A~[~/s~].  ~/~
                      are tied for the highest score.  ~]~]~

          ~#f~[~/We will choose arbitrarily among these.  ~]~

          ~|~%We will induct according to a scheme suggested by ~
          ~#h~[~pg.~/~pg, but modified to accommodate ~*i.~]~

          ~#w~[~/  ~#h~[This suggestion was~/These suggestions were~] ~
          produced using ~*x.~]  ~

          If we let ~ ~pp denote ~@n above then the induction scheme ~
          we'll use is~|~

          ~qs.~

          This induction is justified by the same argument used ~
          to admit ~xj.  ~

          ~#l~[~/Note, however, that the unmeasured ~
                 variable~#m~[ ~&m is~/s ~&m are~] being instantiated.  ~]~

          When applied to the goal at hand the above induction scheme ~
          produces ~#v~[no nontautological subgoals~/one nontautological ~
          subgoal~/the following ~no nontautological subgoals~].~

          ~#t~[~/  However, to achieve this relatively small number of ~
          cases we had to fold ~@n into a single IF-expression.  Had we ~
          left it as a set of clauses this induction would have produced ~
          approximately ~nu cases!  Chances are that this proof attempt ~
          is about to blow up in your face (and all over our memory ~
          boards).~]~|"
          (list (cons #\H (cond ((null induct-hint-val) 2)
                                ((equal induct-hint-val *t*) 1)
                                (t 0)))
                (cons #\n pool-name)
                (cons #\0 len-candidates)
                (cons #\1 (if (int= len-candidates 1) 0 1))
                (cons #\a (if (< len-flushed-candidates
                                 len-candidates)
                              1 0))
                (cons #\2 len-flushed-candidates)
                (cons #\b (if (< len-merged-candidates
                                 len-flushed-candidates)
                              1 0))
                (cons #\3 len-merged-candidates)
                (cons #\4 (if (int= len-merged-candidates 1) 0 1))
                (cons #\c (if (< len-unvetoed-candidates
                                 len-merged-candidates)
                              1 0))
                (cons #\5 (- len-merged-candidates
                             len-unvetoed-candidates))
                (cons #\q len-unvetoed-candidates)
                (cons #\r (zero-one-or-more len-unvetoed-candidates))
                (cons #\6 (if (int= (- len-merged-candidates
                                       len-unvetoed-candidates)
                                    1)
                              0 1))
                (cons #\d (if (< len-complicated-candidates
                                 len-unvetoed-candidates)
                              1 0))
                (cons #\7 len-complicated-candidates)
                (cons #\e (if (< len-high-scoring-candidates
                                 len-complicated-candidates)
                              1 0))
                (cons #\8 len-high-scoring-candidates)
                (cons #\9 (if (int= len-high-scoring-candidates 1) 0 1))
                (cons #\A (if (int= (- len-complicated-candidates
                                       len-high-scoring-candidates)
                                    1)
                              0 1))
                (cons #\f (if (int= len-high-scoring-candidates 1) 0 1))
                (cons #\p p)
                (cons #\s (prettyify-clause-set
                           (induction-formula
                            (list (list p))
                            (access candidate
                                    winning-candidate
                                    :tests-and-alists-lst))
                           (let*-abstractionp state)
                           wrld))
                (cons #\g (access candidate winning-candidate
                                  :xinduction-term))
                (cons #\h (if (access candidate winning-candidate :xancestry)
                              1 0))
                (cons #\i (tilde-*-untranslate-lst-phrase
                           (access candidate winning-candidate :xancestry)
                           nil wrld))
                (cons #\j (ffn-symb
                           (access candidate winning-candidate
                                   :xinduction-term)))
                (cons #\l (if unmeasured-variables 1 0))
                (cons #\m unmeasured-variables)
                (cons #\o (length clauses))
                (cons #\t (if (> estimated-size *maximum-induct-size*)
                              1
                            0))
                (cons #\u estimated-size)
                (cons #\v (if (null clauses) 0 (if (cdr clauses) 2 1)))
                (cons #\w (if (nth 4 attribution-phrase) 1 0))
                (cons #\x attribution-phrase))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
   (increment-timer 'print-time state)))

(defun induct-msg/lose (pool-name induct-hint-val state)

; We print the message that no induction was suggested.

; This function increments timers.  Upon entry, the accumulated time is
; charged to 'prove-time.  The time spent in this function is charged
; to 'print-time.

; Warning: This function should be called under (io? prove ...).

  (pprogn
   (increment-timer 'prove-time state)
   (fms "No induction schemes are suggested by ~#H~[the induction ~
           hint~/~@n~].  Consequently, the proof attempt has ~
           failed.~|"
        (list (cons #\H (cond (induct-hint-val 0)(t 1)))
              (cons #\n pool-name))
        (proofs-co state)
        state
        (term-evisc-tuple nil state))
   (increment-timer 'print-time state)))

; When induct is called it is supplied the hint-settings that were
; attached to the clause by the user.  Induct has the job of loading
; the hint settings into the pspv it returns.  Most of the content of
; the hint-settings is loaded into the rewrite-constant of the pspv.

(defun load-hint-settings-into-rcnst (hint-settings rcnst wrld ctx state)

; Certain user supplied hint settings find their way into the
; rewrite-constant.  They are :expand, :restrict, :hands-off, and
; :in-theory.  Our convention is that if a given hint key/val is
; provided it replaces what was in the rcnst.  Otherwise, we leave the
; corresponding field of rcnst unchanged.

  (er-let* ((new-ens
             (cond
              ((assoc-eq :in-theory hint-settings)
               (load-theory-into-enabled-structure
                :from-hint
                (cdr (assoc-eq :in-theory hint-settings))
                nil
                (access rewrite-constant rcnst :current-enabled-structure)
                t
                nil
                wrld ctx state))
              (t (value (access rewrite-constant rcnst
                                :current-enabled-structure))))))
           (value (change rewrite-constant rcnst
                          :expand-lst
                          (cond
                           ((assoc-eq :expand hint-settings)
                            (cdr (assoc-eq :expand hint-settings)))
                           (t (access rewrite-constant rcnst :expand-lst)))
                          :restrictions-alist
                          (cond
                           ((assoc-eq :restrict hint-settings)
                            (cdr (assoc-eq :restrict hint-settings)))
                           (t (access rewrite-constant rcnst
                                      :restrictions-alist)))
                          :fns-to-be-ignored-by-rewrite
                          (cond
                           ((assoc-eq :hands-off hint-settings)
                            (cdr (assoc-eq :hands-off hint-settings)))
                           (t (access rewrite-constant rcnst
                                      :fns-to-be-ignored-by-rewrite)))
                          :current-enabled-structure
                          new-ens
                          :nonlinearp
                          (cond
                           ((assoc-eq :nonlinearp hint-settings)
                            (cdr (assoc-eq :nonlinearp hint-settings)))
                           (t (access rewrite-constant rcnst :nonlinearp)))))))

(defun update-hint-settings (new-hint-settings old-hint-settings)
  (cond
   ((endp new-hint-settings) old-hint-settings)
   ((assoc-eq (caar new-hint-settings) old-hint-settings)
    (update-hint-settings
     (cdr new-hint-settings)
     (cons (car new-hint-settings)
           (delete-assoc-eq (caar new-hint-settings)
                            old-hint-settings))))
   (t (update-hint-settings
       (cdr new-hint-settings)
       (cons (car new-hint-settings) old-hint-settings)))))

; Thus, a given hint-settings causes us to modify the pspv as follows:

(defun load-hint-settings-into-pspv (increment-flg hint-settings pspv wrld ctx
                                                   state)

; We load the hint-settings into the rewrite-constant of pspv, thereby
; making available the :expand, :restrict, :hands-off, and :in-theory
; hint settings.  We also store the hint-settings in the hint-settings
; field of the pspv, making available the :induct and :do-not-induct
; hint settings.

; When increment-flg is non-nil, we want to preserve the input pspv's hint
; settings except when they collide with hint-settings.  Otherwise (for
; example, when induct is called), we completely replace the input pspv's
; :hint-settings with hint-settings.

; Warning: Restore-hint-settings-in-pspv, below, is supposed to undo
; these changes while not affecting the rest of a newly obtained pspv.
; Keep these two functions in step.

  (er-let* ((rcnst (load-hint-settings-into-rcnst
                    hint-settings
                    (access prove-spec-var pspv :rewrite-constant)
                    wrld ctx state)))
           (value
            (change prove-spec-var pspv
                    :rewrite-constant rcnst
                    :hint-settings
                    (if increment-flg
                        (update-hint-settings hint-settings
                                              (access prove-spec-var pspv
                                                      :hint-settings))
                      hint-settings)))))

(defun restore-hint-settings-in-pspv (new-pspv old-pspv)

; This considers the fields changed by load-hint-settings-into-pspv above
; and restores them in new-pspv to the values they have in old-pspv.  The
; Idea is that we start with a pspv1, load hints into it to get pspv2,
; pass that around the prover and obtain pspv3 (which has a new tag tree
; and pool etc), and then restore the hint settings as they were in pspv1.
; In this example, new-pspv would be pspv3 and old-pspv would be pspv1.

  (change prove-spec-var new-pspv
          :rewrite-constant (access prove-spec-var old-pspv :rewrite-constant)
          :hint-settings (access prove-spec-var old-pspv :hint-settings)))

(defun remove-trivial-clauses (clauses wrld)
  (cond
   ((null clauses) nil)
   ((trivial-clause-p (car clauses) wrld)
    (remove-trivial-clauses (cdr clauses) wrld))
   (t (cons (car clauses)
            (remove-trivial-clauses (cdr clauses) wrld)))))

#+:non-standard-analysis
(defun classicalp (fn wrld)

; WARNING: This function is expected to return t for fn = :?, in support of
; measures (:? v1 ... vk), since classicalp is called by
; get-non-classical-fns-from-list in support of get-non-classical-fns-aux.

  (getprop fn 'classicalp

; We guarantee a 'classicalp property of nil for all non-classical
; functions.  We make no claims about the existence of a 'classicalp
; property for classical functions; in fact, as of Version_2.5 our
; intention is to put no 'classicalp property for classical functions.

           t 
           'current-acl2-world wrld))

;; RAG - This function tests whether a list of names is made up purely
;; of classical function names (i.e., not descended from the
;; non-standard function symbols)

#+:non-standard-analysis
(defun classical-fn-list-p (names wrld)
  (cond ((null names) t)
        ((not (classicalp (car names) wrld))
         nil)
        (t (classical-fn-list-p (cdr names) wrld))))
     
#+:non-standard-analysis
(defun non-standard-vector-check (vars accum)
  (if (null vars)
      accum
    (non-standard-vector-check (cdr vars)
                               (cons (mcons-term* 'standard-numberp (car vars))
                                     accum))))

#+:non-standard-analysis
(defun merge-ns-check (checks clause accum)
  (if (null checks)
      accum
    (merge-ns-check (cdr checks) clause (cons (cons (car checks)
                                                    clause)
                                              accum))))

#+:non-standard-analysis
(defun trap-non-standard-vector-aux (cl-set accum-cl checks wrld)
  (cond ((null cl-set) accum-cl)
        ((classical-fn-list-p (all-fnnames-lst (car cl-set)) wrld)
         (trap-non-standard-vector-aux (cdr cl-set) accum-cl checks wrld))
        (t 
         (trap-non-standard-vector-aux (cdr cl-set)
                                       (append (merge-ns-check checks
                                                               (car cl-set)
                                                               nil)
                                               accum-cl)
                                       checks
                                       wrld))))

#+:non-standard-analysis
(defun remove-adjacent-duplicates (lst)
  (cond ((or (null lst) (null (cdr lst))) lst)
        ((equal (car lst) (car (cdr lst)))
         (remove-adjacent-duplicates (cdr lst)))
        (t (cons (car lst) (remove-adjacent-duplicates (cdr lst))))))

#+:non-standard-analysis
(defun non-standard-induction-vars (candidate wrld)
  (remove-adjacent-duplicates
   (merge-sort-term-order
    (append (access candidate candidate :changed-vars)

; The following line was changed after Version_3.0.1.  It seems like a correct
; change, but we'll leave this comment here until Ruben Gamboa (ACL2(r) author)
; checks this change.

            (measured-variables candidate wrld)))))

#+:non-standard-analysis
(defun trap-non-standard-vector (cl-set candidate accum-cl wrld)
  (trap-non-standard-vector-aux cl-set accum-cl 
                                (non-standard-vector-check
                                 (non-standard-induction-vars
                                  candidate wrld)
                                 nil)
                                wrld))

(defun induct (pool-name cl-set hint-settings pspv wrld ctx state)

; We take a set of clauses, cl-set, and return four values.  The first
; is either the signal 'lose (meaning we could find no induction to do
; and have explained that to the user) or 'continue, meaning we're
; going to use induction.  The second value is a list of clauses,
; representing the induction base cases and steps.  The last two
; things are new values for pspv and state.  We modify pspv to store
; the induction-hyp-terms and induction-concl-terms for the
; simplifier.

; The clause set we explore to collect the induction candidates,
; x-cl-set, is not necessarily cl-set.  If the value, v, of :induct in
; the hint-settings is non-nil and non-*t*, then we explore the clause
; set {{v}} for candidates.

  (let ((induct-hint-val
         (cdr (assoc-eq :induct hint-settings))))
    (mv-let
     (erp new-pspv state)
     (load-hint-settings-into-pspv
                 nil
                 (if induct-hint-val
                     (delete-assoc-eq :induct hint-settings)
                   hint-settings)
                 pspv wrld ctx state)
     (cond
      (erp (mv 'lose nil pspv state))
      (t
       (let* ((candidates
               (get-induction-cands-from-cl-set
                (select-x-cl-set cl-set induct-hint-val)
                new-pspv wrld state))
              (flushed-candidates
               (m&m candidates 'flush-candidates))

; In nqthm we flushed and merged at the same time.  However, flushing
; is a mate and merge function that has the distributive and non-preclusion
; properties and hence can be done with a simple m&m.  Merging on the other
; hand is preclusive and so we wait and run m&m-over-powerset to do
; that.  In nqthm, we did preclusive merging with m&m (then called
; TRANSITIVE-CLOSURE) and just didn't worry about the fact that we
; messed up some potential merges by earlier merges.  Of course, the
; powerset computation is so expensive for large sets that we can't
; just go into it blindly, so we don't use the m&m-over-powerset to do
; flushing and merging at the same time.  Flushing eliminates duplicates
; and subsumed inductions and thus shrinks the set as much as we know how.

              (merged-candidates
               (cond ((< (length flushed-candidates) 10)
                      (m&m-over-powerset flushed-candidates 'merge-candidates))
                     (t (m&m flushed-candidates 'merge-candidates))))

; Note: We really respect powerset.  If the set we're trying to merge
; has more than 10 things in it -- an arbitrary choice at the time of
; this writing -- we just do the m&m instead, which causes us to miss
; some merges because we only use each candidate once and merging
; early merges can prevent later ones.

              (unvetoed-candidates
               (compute-vetoes merged-candidates wrld))

              (complicated-candidates
               (maximal-elements unvetoed-candidates 'induction-complexity wrld))

              (high-scoring-candidates
               (maximal-elements complicated-candidates 'score wrld))
              (winning-candidate (car high-scoring-candidates)))
         (cond
          (winning-candidate
           (mv-let
            (erp candidate-ttree state)
            (accumulate-ttree-into-state
             (access candidate winning-candidate :ttree)
             state)
            (declare (ignore erp))
            (let* (

; First, we estimate the size of the answer if we persist in using cl-set.

                   (estimated-size
                    (induction-formula-size cl-set
                                            (access candidate
                                                    winning-candidate
                                                    :tests-and-alists-lst)))

; Next we create clauses, the set of clauses we wish to prove.
; Observe that if the estimated size is greater than
; *maximum-induct-size* we squeeze the cl-set into the form {{p}},
; where p is a single term.  This eliminates the combinatoric
; explosion at the expense of making the rest of the theorem prover
; suffer through opening things back up.  The idea, however, is that
; it is better to give the user something to look at, so he see's the
; problem blowing up in front of him in rewrite, than to just
; disappear into induction and never come out.  We have seen simple
; cases where failed guard conjectures would have led to inductions
; containing thousands of cases had induct been allowed to compute
; them out.

                   (clauses0
                    (induction-formula
                     (cond ((> estimated-size *maximum-induct-size*)
                            (list (list (termify-clause-set cl-set))))
                           (t cl-set))
                     (access candidate winning-candidate :tests-and-alists-lst)))
                   (clauses1
                    #+:non-standard-analysis
                    (trap-non-standard-vector cl-set
                                              winning-candidate
                                              clauses0
                                              wrld)
                    #-:non-standard-analysis
                    clauses0)
                   (clauses
                    (cond ((> estimated-size *maximum-induct-size*)
                           clauses1)
                          (t (remove-trivial-clauses clauses1 wrld))))

; Now we inform the simplifier of this induction and store the ttree of
; the winning candidate into the tag-tree of the pspv.

                   (newer-pspv
                    (inform-simplify
                     (access candidate winning-candidate :tests-and-alists-lst)
                     (cons (access candidate winning-candidate :xinduction-term)
                           (access candidate winning-candidate :xother-terms))
                     (change prove-spec-var new-pspv
                             :tag-tree
                             (cons-tag-trees
                              candidate-ttree
                              (access prove-spec-var new-pspv :tag-tree))))))

; Now we print out the induct message.

              (let ((state
                     (io? prove nil state
                          (wrld clauses estimated-size winning-candidate
                                high-scoring-candidates complicated-candidates
                                unvetoed-candidates merged-candidates
                                flushed-candidates candidates induct-hint-val
                                cl-set pool-name)
                          (induct-msg/continue pool-name
                                               cl-set
                                               induct-hint-val
                                               (length candidates)
                                               (length flushed-candidates)
                                               (length merged-candidates)
                                               (length unvetoed-candidates)
                                               (length complicated-candidates)
                                               (length high-scoring-candidates)
                                               winning-candidate
                                               estimated-size
                                               clauses
                                               wrld
                                               state))))
                (mv 'continue
                    clauses
                    newer-pspv
                    state)))))
          (t

; Otherwise, we report our failure to find an induction and return the
; 'lose signal.

           (let ((state (io? prove nil state
                             (induct-hint-val pool-name)
                             (induct-msg/lose pool-name induct-hint-val state))))
             (mv 'lose nil pspv state))))))))))

; We now define the elimination of irrelevance.  Logically this ought
; to be defined when the other processors are defined.  But to
; partition the literals of the clause by variables we use m&m, which
; is not defined until induction.  We could have moved m&m-apply back
; into the earlier processors, but that would require moving about a
; third of induction back there.  So we have just put all of
; irrelevance elimination here.

(defun pair-vars-with-lits (cl)

; We pair each lit of clause cl with its variables.  The variables are
; in the car of the pair, the singleton set containing the lit is in
; the cdr.

  (cond ((null cl) nil)
        (t (cons (cons (all-vars (car cl)) (list (car cl)))
                 (pair-vars-with-lits (cdr cl))))))


(mutual-recursion

(defun ffnnames-subsetp (term lst)

; Collect the ffnames in term and say whether it is a subset of lst.
; We don't consider fnnames of constants, e.g., the cons of '(a b).

  (cond ((variablep term) t)
        ((fquotep term) t)
        ((flambda-applicationp term)
         (and (ffnnames-subsetp-listp (fargs term) lst)
              (ffnnames-subsetp (lambda-body term) lst)))
        ((member-eq (ffn-symb term) lst)
         (ffnnames-subsetp-listp (fargs term) lst))
        (t nil)))

(defun ffnnames-subsetp-listp (terms lst)
  (cond ((null terms) t)
        ((ffnnames-subsetp (car terms) lst)
         (ffnnames-subsetp-listp (cdr terms) lst))
        (t nil)))
)

;; RAG - I added realp and complexp to the list of function names
;; simplification can decide.

(defun probably-not-validp (cl)

; Cl is a clause.  We return t if we think there is an instantiation
; of cl that makes each literal false.  It is assumed that cl has
; survived simplification.

; We have two trivial heuristics.  One is to detect whether the only
; function symbols in cl are ones that we think make up a fragment
; of the theory that simplification can decide.  The other heuristic
; is to bet that any cl consisting of a single literal which is of the
; form (fn v1 ... vn) or (not (fn v1 ... vn)), where the vi are
; distinct variables, is probably not valid.

; It's pretty bold to include a recursive function, namely true-listp, in the
; list below.  However, as long as it's the only one, we feel safe.

  (or (ffnnames-subsetp-listp cl '(consp integerp rationalp
                                         #+:non-standard-analysis realp 
                                         acl2-numberp
                                         true-listp complex-rationalp 
                                         #+:non-standard-analysis complexp
                                         stringp characterp
                                         symbolp cons car cdr equal
                                         binary-+ unary-- < apply))
      (case-match cl
                  ((('not (& . args)))
                   (and (all-variablep args)
                        (no-duplicatesp-equal args)))
                  (((& . args))
                   (and (all-variablep args)
                        (no-duplicatesp-equal args)))
                  (& nil))))

(defun irrelevant-lits (alist)

; Alist is an alist that associates a set of literals with each key.
; The keys are irrelevant.  We consider each set of literals and decide
; if it is probably not valid.  If so we consider it irrelevant.
; We return the concatenation of all the irrelevant literal sets.

  (cond ((null alist) nil)
        ((probably-not-validp (cdar alist))
         (append (cdar alist) (irrelevant-lits (cdr alist))))
        (t (irrelevant-lits (cdr alist)))))

(defun eliminate-irrelevance-clause (cl hist pspv wrld state)

; A standard clause processor of the waterfall.

; We return 4 values.  The first is a signal that is either 'hit, or
; 'miss.  When the signal is 'miss, the other 3 values are irrelevant.
; When the signal is 'hit, the second result is the list of new
; clauses, the third is a ttree that will become that component of the
; history-entry for this elimination, and the fourth is an
; unmodified pspv.  (We return the fourth thing to adhere to the
; convention used by all clause processors in the waterfall (q.v.).)

  (declare (ignore hist wrld state))
  (cond
   ((not (assoc-eq 'being-proved-by-induction
                   (access prove-spec-var pspv :pool)))
    (mv 'miss nil nil nil))
   (t (let* ((partitioning (m&m (pair-vars-with-lits cl)
                                'intersectp-eq/union-equal))
             (irrelevant-lits (irrelevant-lits partitioning)))
        (cond ((null irrelevant-lits)
               (mv 'miss nil nil nil))
              (t (mv 'hit
                     (list (set-difference-equal cl irrelevant-lits))
                     (add-to-tag-tree
                      'irrelevant-lits irrelevant-lits
                      (add-to-tag-tree
                       'clause cl nil))
                     pspv)))))))

(defun eliminate-irrelevance-clause-msg1 (signal clauses ttree pspv state)

; The arguments to this function are the standard ones for an output
; function in the waterfall.  See the discussion of the waterfall.

  (declare (ignore signal pspv clauses))
  (let* ((lits (cdr (tagged-object 'irrelevant-lits ttree)))
         (clause (cdr (tagged-object 'clause ttree)))
         (concl (car (last clause))))
    (cond
     ((equal (length lits)
             (length clause))
      (fms "We suspect that this conjecture is not a theorem.  We ~
            might as well be trying to prove~|"
           nil
           (proofs-co state)
           state
           (term-evisc-tuple nil state)))
     (t
      (let ((iterms (cond
                     ((member-equal concl lits)
                      (append
                       (dumb-negate-lit-lst
                        (remove1-equal concl lits))
                       (list concl)))
                     (t (dumb-negate-lit-lst lits)))))
        (fms "We suspect that the term~#0~[ ~*1 is~/s ~*1 are~] ~
            irrelevant to the truth of this conjecture and throw ~
            ~#0~[it~/them~] out.  We will thus try to prove~|"
             (list
              (cons #\0 iterms)
              (cons #\1 (tilde-*-untranslate-lst-phrase iterms t (w state))))
             (proofs-co state)
             state
             (term-evisc-tuple nil state)))))))