/[mojave]/metaprl/theories/czf/czf_itt_group.prla
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_group.prla

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3405 by xiny, Sun Sep 23 07:33:50 2001 UTC revision 3463 by nogin, Sat Dec 8 03:17:49 2001 UTC
# Line 2541  Line 2541 
2541  B       b972    t972  B       b972    t972
2542  T       t973    o937 b972 b4 b969  T       t973    o937 b972 b4 b969
2543  B       b973    t973  B       b973    t973
2544    T       t1      o b973 b4
2545    B       b1      t1
2546    T       t2      o b970 b1
2547    B       b2      t2
2548    T       t3      o936 b960 b2
2549    B       b3      t3
2550  P       p973    String wf  P       p973    String wf
2551  O       o973    tactic_arg p973  O       o973    tactic_arg p973
2552  B       b974    t949 v_2  B       b974    t949 v_2
# Line 2582  Line 2588 
2588  B       b985    t985  B       b985    t985
2589  T       t986    o973 b976 b4 b985  T       t986    o973 b976 b4 b985
2590  B       b986    t986  B       b986    t986
 T       t987    o b986 b4  
 B       b987    t987  
 T       t988    o b973 b987  
 B       b988    t988  
 T       t989    o b970 b988  
 B       b989    t989  
 T       t990    o936 b960 b989  
 B       b990    t990  
2591  P       p990    String autoT  P       p990    String autoT
2592  O       o990    ext_rule p990  O       o990    ext_rule p990
2593  T       t991    o936 b970 b4  T       t991    o936 b970 b4
# Line 2619  Line 2617 
2617  B       b999    t999  B       b999    t999
2618  T       t1000   o937 b999 b4 b996  T       t1000   o937 b999 b4 b996
2619  B       b1000   t1000  B       b1000   t1000
2620    T       t214    o b1000 b4
2621    B       b214    t214
2622    T       t215    o b997 b214
2623    B       b215    t215
2624    T       t218    o936 b973 b215
2625    B       b218    t218
2626  B       b1001   t966 v_3  B       b1001   t966 v_3
2627  T       t1001   o711 b1001  T       t1001   o711 b1001
2628  S       s1001   t620 h h947 h957 h971  S       s1001   t620 h h947 h957 h971
# Line 2644  Line 2648 
2648  B       b1009   t1008  B       b1009   t1008
2649  T       t1009   o973 b1003 b4 b1009  T       t1009   o973 b1003 b4 b1009
2650  B       b1010   t1009  B       b1010   t1009
 T       t1010   o b1010 b4  
 B       b1011   t1010  
 T       t1011   o b1000 b1011  
 B       b1012   t1011  
 T       t1012   o b997 b1012  
 B       b1013   t1012  
 T       t1013   o936 b973 b1013  
 B       b1014   t1013  
2651  T       t1014   o936 b997 b4  T       t1014   o936 b997 b4
2652  B       b1015   t1014  B       b1015   t1014
2653  T       t1015   o990 b935 b1015 b4 b4  T       t1015   o990 b935 b1015 b4 b4
# Line 2690  Line 2686 
2686  B       b1027   t1026  B       b1027   t1026
2687  T       t1027   o937 b1026 b4 b1027  T       t1027   o937 b1026 b4 b1027
2688  B       b1028   t1027  B       b1028   t1027
2689    T       t219    o b1028 b4
2690    B       b219    t219
2691    T       t229    o936 b1022 b219
2692    B       b229    t229
2693  B       b1029   t1017 v_5  B       b1029   t1017 v_5
2694  T       t1029   o711 b1029  T       t1029   o711 b1029
2695  S       s1029   t620 h h947 h957 h971 h998 h1018  S       s1029   t620 h h947 h957 h971 h998 h1018
# Line 2715  Line 2715 
2715  B       b1037   t1036  B       b1037   t1036
2716  T       t1037   o973 b1031 b4 b1037  T       t1037   o973 b1031 b4 b1037
2717  B       b1038   t1037  B       b1038   t1037
 T       t1038   o b1038 b4  
 B       b1039   t1038  
 T       t1039   o b1028 b1039  
 B       b1040   t1039  
 T       t1040   o936 b1022 b1040  
 B       b1041   t1040  
2718  P       p1041   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"  P       p1041   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2719  O       o1041   ext_rule p1041  O       o1041   ext_rule p1041
2720  H       h1041   v_6 t925  H       h1041   v_6 t925
# Line 2780  Line 2774 
2774  B       b1063   t1062  B       b1063   t1062
2775  T       t1063   o1041 b935 b1047 b1050 b1063  T       t1063   o1041 b935 b1047 b1050 b1063
2776  B       b1064   t1063  B       b1064   t1063
2777    T       t230    o b1064 b4
2778    B       b230    t230
2779  T       t1064   o936 b1038 b4  T       t1064   o936 b1038 b4
2780  B       b1065   t1064  B       b1065   t1064
2781  T       t1065   o1050 b935 b1065 b4 b4  T       t1065   o1050 b935 b1065 b4 b4
2782  B       b1066   t1065  B       b1066   t1065
2783  T       t1066   o b1066 b4  T       t1066   o b1066 b4
2784  B       b1067   t1066  B       b1067   t1066
2785  T       t1067   o b1064 b1067  T       t233    o1024 b935 b229 b230 b1067
2786  B       b1068   t1067  B       b233    t233
2787  T       t1068   o1024 b935 b1041 b1068 b4  T       t237    o b233 b4
2788  B       b1069   t1068  B       b237    t237
2789  T       t1069   o b1069 b4  T       t238    o1016 b935 b1024 b237 b4
2790  B       b1070   t1069  B       b238    t238
2791  T       t1070   o1016 b935 b1024 b1070 b4  T       t239    o b238 b4
2792  B       b1071   t1070  B       b239    t239
2793    T       t242    o b1016 b239
2794    B       b242    t242
2795  P       p1071   String "rwh unfold_fun_set 0 thenT autoT"  P       p1071   String "rwh unfold_fun_set 0 thenT autoT"
2796  O       o1071   ext_rule p1071  O       o1071   ext_rule p1071
2797  T       t1071   o936 b1010 b4  T       t1071   o936 b1010 b4
# Line 2802  Line 2800 
2800  B       b1073   t1072  B       b1073   t1072
2801  T       t1073   o b1073 b4  T       t1073   o b1073 b4
2802  B       b1074   t1073  B       b1074   t1073
2803  T       t1074   o b1071 b1074  T       t243    o992 b935 b218 b242 b1074
2804  B       b1075   t1074  B       b243    t243
2805  T       t1075   o b1016 b1075  T       t251    o b243 b4
2806  B       b1076   t1075  B       b251    t251
2807  T       t1076   o992 b935 b1014 b1076 b4  T       t256    o b992 b251
2808  B       b1077   t1076  B       b256    t256
2809  T       t1077   o936 b986 b4  T       t1077   o936 b986 b4
2810  B       b1078   t1077  B       b1078   t1077
2811  T       t1078   o1071 b935 b1078 b4 b4  T       t1078   o1071 b935 b1078 b4 b4
2812  B       b1079   t1078  B       b1079   t1078
2813  T       t1079   o b1079 b4  T       t1079   o b1079 b4
2814  B       b1080   t1079  B       b1080   t1079
2815  T       t1080   o b1077 b1080  T       t257    o965 b935 b3 b256 b1080
2816  B       b1081   t1080  B       b257    t257
2817  T       t1081   o b992 b1081  T       t265    o b257 b4
2818  B       b1082   t1081  B       b265    t265
2819  T       t1082   o965 b935 b990 b1082 b4  T       t266    o b965 b265
2820  B       b1083   t1082  B       b266    t266
 T       t1083   o b1083 b4  
 B       b1084   t1083  
 T       t1084   o b965 b1084  
 B       b1085   t1084  
2821  NSummary!ext_goal       ext_goal        ext_goal Summary  NSummary!ext_goal       ext_goal        ext_goal Summary
2822  O       o1085   ext_goal  O       o1085   ext_goal
2823  S       s1085   t620 h  S       s1085   t620 h
# Line 3322  Line 3316 
3316  B       b1292   t1291  B       b1292   t1291
3317  T       t1292   o937 b1291 b4 b1292  T       t1292   o937 b1291 b4 b1292
3318  B       b1293   t1292  B       b1293   t1292
3319    T       t268    o b1293 b4
3320    B       b268    t268
3321    T       t269    o936 b1289 b268
3322    B       b269    t269
3323  B       b1294   t949 v_1  B       b1294   t949 v_1
3324  T       t1294   o711 b1294  T       t1294   o711 b1294
3325  S       s1294   t620 h h1264 h1265 h1266 h1267  S       s1294   t620 h h1264 h1265 h1266 h1267
# Line 3343  Line 3341 
3341  B       b1301   t1300  B       b1301   t1300
3342  T       t1301   o973 b1296 b4 b1301  T       t1301   o973 b1296 b4 b1301
3343  B       b1302   t1301  B       b1302   t1301
 T       t1302   o b1302 b4  
 B       b1303   t1302  
 T       t1303   o b1293 b1303  
 B       b1304   t1303  
 T       t1304   o936 b1289 b1304  
 B       b1305   t1304  
3344  P       p1305   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"  P       p1305   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3345  O       o1305   ext_rule p1305  O       o1305   ext_rule p1305
3346  T       t1305   o676 b966 b993  T       t1305   o676 b966 b993
# Line 3362  Line 3354 
3354  B       b1308   t1307  B       b1308   t1307
3355  T       t1308   o937 b1307 b4 b1308  T       t1308   o937 b1307 b4 b1308
3356  B       b1309   t1308  B       b1309   t1308
3357    T       t270    o b1309 b4
3358    B       b270    t270
3359    T       t273    o936 b1293 b270
3360    B       b273    t273
3361  B       b1310   t966 v_2  B       b1310   t966 v_2
3362  T       t1310   o711 b1310  T       t1310   o711 b1310
3363  S       s1310   t620 h h1264 h1265 h1266 h1267 h1289  S       s1310   t620 h h1264 h1265 h1266 h1267 h1289
# Line 3383  Line 3379 
3379  B       b1317   t1316  B       b1317   t1316
3380  T       t1317   o973 b1312 b4 b1317  T       t1317   o973 b1312 b4 b1317
3381  B       b1318   t1317  B       b1318   t1317
 T       t1318   o b1318 b4  
 B       b1319   t1318  
 T       t1319   o b1309 b1319  
 B       b1320   t1319  
 T       t1320   o936 b1293 b1320  
 B       b1321   t1320  
3382  P       p1321   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"  P       p1321   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3383  O       o1321   ext_rule p1321  O       o1321   ext_rule p1321
3384  T       t1321   o676 b1017 b1018  T       t1321   o676 b1017 b1018
# Line 3419  Line 3409 
3409  B       b1330   t1329  B       b1330   t1329
3410  T       t1330   o937 b1329 b4 b1330  T       t1330   o937 b1329 b4 b1330
3411  B       b1331   t1330  B       b1331   t1330
3412    T       t274    o b1331 b4
3413    B       b274    t274
3414    T       t289    o936 b1325 b274
3415    B       b289    t289
3416  S       s1331   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321  S       s1331   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3417  G       s1331   t1144  G       s1331   t1144
3418  B       b1332   s1331  B       b1332   s1331
# Line 3438  Line 3432 
3432  B       b1338   t1337  B       b1338   t1337
3433  T       t1338   o973 b1333 b4 b1338  T       t1338   o973 b1333 b4 b1338
3434  B       b1339   t1338  B       b1339   t1338
 T       t1339   o b1339 b4  
 B       b1340   t1339  
 T       t1340   o b1331 b1340  
 B       b1341   t1340  
 T       t1341   o936 b1325 b1341  
 B       b1342   t1341  
3435  P       p1342   String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"  P       p1342   String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3436  O       o1342   ext_rule p1342  O       o1342   ext_rule p1342
3437  T       t1342   o936 b1331 b4  T       t1342   o936 b1331 b4
3438  B       b1343   t1342  B       b1343   t1342
3439  T       t1343   o1342 b935 b1343 b4 b4  T       t1343   o1342 b935 b1343 b4 b4
3440  B       b1344   t1343  B       b1344   t1343
3441    T       t290    o b1344 b4
3442    B       b290    t290
3443    T       t292    o936 b1339 b4
3444    B       b292    t292
3445    T       t300    o1071 b935 b292 b4 b4
3446    B       b300    t300
3447    T       t301    o b300 b4
3448    B       b301    t301
3449    T       t304    o1327 b935 b289 b290 b301
3450    B       b304    t304
3451    T       t309    o b304 b4
3452    B       b309    t309
3453    T       t310    o1321 b935 b1327 b309 b4
3454    B       b310    t310
3455    T       t315    o b310 b4
3456    B       b315    t315
3457  H       h1344   s1 t1169  H       h1344   s1 t1169
3458  T       t1344   o738 b560 b561  T       t1344   o738 b560 b561
3459  H       h1345   x t1344  H       h1345   x t1344
 T       t1345   o738 b1018 b1018  
 S       s1345   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224 h1345  
 G       s1345   t1345  
 B       b1345   s1345  
 T       t1346   o938 b1345 b1107  
 B       b1346   t1346  
3460  B       b1347   t1344  B       b1347   t1344
 B       b1348   t1345  
 T       t1348   o1177 b1347 b1348  
 S       s1348   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224  
 G       s1348   t1348  
 B       b1349   s1348  
 T       t1349   o938 b1349 b1107  
 B       b1350   t1349  
 B       b1351   t1348 s2  
 T       t1351   o1185 b1186 b1351  
 S       s1351   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344  
 G       s1351   t1351  
 B       b1352   s1351  
 T       t1352   o938 b1352 b1107  
 B       b1353   t1352  
 B       b1354   t1351 s1  
 T       t1354   o1185 b1186 b1354  
 S       s1354   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321  
 G       s1354   t1354  
 B       b1355   s1354  
 T       t1355   o938 b1355 b1107  
 B       b1356   t1355  
 T       t1356   o2 b1339  
 B       b1357   t1356  
 T       t1357   o973 b1356 b983 b1357  
 B       b1358   t1357  
 T       t1358   o2 b1358  
 B       b1359   t1358  
 T       t1359   o937 b1353 b983 b1359  
 B       b1360   t1359  
 T       t1360   o2 b1360  
 B       b1361   t1360  
 T       t1361   o937 b1350 b983 b1361  
 B       b1362   t1361  
 T       t1362   o2 b1362  
 B       b1363   t1362  
 T       t1363   o937 b1346 b4 b1363  
 B       b1364   t1363  
 T       t1364   o b1364 b4  
 B       b1365   t1364  
 T       t1365   o936 b1339 b1365  
 B       b1366   t1365  
 T       t1366   o1085 b1364  
 B       b1367   t1366  
 T       t1367   o b1367 b4  
 B       b1368   t1367  
 T       t1368   o1071 b935 b1366 b1368 b4  
 B       b1369   t1368  
 T       t1369   o b1369 b4  
 B       b1370   t1369  
 T       t1370   o b1344 b1370  
 B       b1371   t1370  
 T       t1371   o1327 b935 b1342 b1371 b4  
 B       b1372   t1371  
 T       t1372   o b1372 b4  
 B       b1373   t1372  
 T       t1373   o1321 b935 b1327 b1373 b4  
 B       b1374   t1373  
3461  T       t1374   o936 b1318 b4  T       t1374   o936 b1318 b4
3462  B       b1375   t1374  B       b1375   t1374
3463  T       t1375   o1071 b935 b1375 b4 b4  T       t1375   o1071 b935 b1375 b4 b4
3464  B       b1376   t1375  B       b1376   t1375
 T       t1376   o b1376 b4  
 B       b1377   t1376  
 T       t1377   o b1374 b1377  
 B       b1378   t1377  
3465  P       p1378   String "eqSetSymT thenT autoT"  P       p1378   String "eqSetSymT thenT autoT"
3466  O       o1378   ext_rule p1378  O       o1378   ext_rule p1378
3467  T       t1378   o676 b949 b993  T       t1378   o676 b949 b993
# Line 3566  Line 3503 
3503  B       b1394   t1393  B       b1394   t1393
3504  T       t1394   o b1394 b4  T       t1394   o b1394 b4
3505  B       b1395   t1394  B       b1395   t1394
3506  T       t1395   o1305 b935 b1321 b1378 b1395  T       t316    o b1376 b1395
3507  B       b1396   t1395  B       b316    t316
3508    T       t318    o1305 b935 b273 b315 b316
3509    B       b318    t318
3510    T       t320    o b318 b4
3511    B       b320    t320
3512  T       t1396   o936 b1302 b4  T       t1396   o936 b1302 b4
3513  B       b1397   t1396  B       b1397   t1396
3514  T       t1397   o1071 b935 b1397 b4 b4  T       t1397   o1071 b935 b1397 b4 b4
3515  B       b1398   t1397  B       b1398   t1397
 T       t1398   o b1398 b4  
 B       b1399   t1398  
 T       t1399   o b1396 b1399  
 B       b1400   t1399  
3516  T       t1400   o676 b948 b966  T       t1400   o676 b948 b966
3517  S       s1400   t620 h h1264 h1265 h1266 h1267  S       s1400   t620 h h1264 h1265 h1266 h1267
3518  G       s1400   t1400  G       s1400   t1400
# Line 3615  Line 3552 
3552  B       b1416   t1415  B       b1416   t1415
3553  T       t1416   o b1416 b4  T       t1416   o b1416 b4
3554  B       b1417   t1416  B       b1417   t1416
3555  T       t1417   o1264 b935 b1305 b1400 b1417  T       t327    o b1398 b1417
3556  B       b1418   t1417  B       b327    t327
3557  T       t1418   o b1418 b4  T       t331    o1264 b935 b269 b320 b327
3558  B       b1419   t1418  B       b331    t331
3559  T       t1419   o b1264 b1419  T       t332    o b331 b4
3560  B       b1420   t1419  B       b332    t332
3561  T       t1420   o b1091 b1420  T       t335    o b1264 b332
3562  B       b1421   t1420  B       b335    t335
3563  T       t1421   o934 b935 b963 b1085 b1421  T       t339    o b1091 b335
3564  B       b1422   t1421  B       b339    t339
3565  T       t1422   o933 b1422  T       t340    o934 b935 b963 b266 b339
3566  B       b1423   t1422  B       b340    t340
3567    T       t359    o933 b340
3568    B       b359    t359
3569  P       p1423   Number 5390  P       p1423   Number 5390
3570  P       p1424   Number 5398  P       p1424   Number 5398
3571  O       o1424   resource_defs p1423 p1424 p264  O       o1424   resource_defs p1423 p1424 p264
# Line 3640  Line 3579 
3579  B       b1427   t1427  B       b1427   t1427
3580  T       t1428   o b1427 b4  T       t1428   o b1427 b4
3581  B       b1428   t1428  B       b1428   t1428
3582  T       t1429   o919 b922 b933 b1423 b1428  T       t370    o919 b922 b933 b359 b1428
3583  B       b1429   t1429  B       b370    t370
3584  T       t1430   o918 b1429  T       t385    o918 b370
3585  B       b1430   t1430  B       b385    t385
3586  P       p1430   Number 5838  P       p1430   Number 5838
3587  P       p1431   Number 6264  P       p1431   Number 6264
3588  O       o1431   location p1430 p1431  O       o1431   location p1430 p1431
# Line 3761  Line 3700 
3700  B       b1478   t1477  B       b1478   t1477
3701  T       t1478   o937 b1477 b4 b1478  T       t1478   o937 b1477 b4 b1478
3702  B       b1479   t1478  B       b1479   t1478
3703    T       t391    o b1479 b4
3704    B       b391    t391
3705    T       t392    o936 b1468 b391
3706    B       b392    t392
3707  B       b1480   t1456 v_2  B       b1480   t1456 v_2
3708  T       t1480   o711 b1480  T       t1480   o711 b1480
3709  S       s1480   t620 h h1454 h1465  S       s1480   t620 h h1454 h1465
# Line 3782  Line 3725 
3725  B       b1487   t1486  B       b1487   t1486
3726  T       t1487   o973 b1482 b4 b1487  T       t1487   o973 b1482 b4 b1487
3727  B       b1488   t1487  B       b1488   t1487
 T       t1488   o b1488 b4  
 B       b1489   t1488  
 T       t1489   o b1479 b1489  
 B       b1490   t1489  
 T       t1490   o936 b1468 b1490  
 B       b1491   t1490  
3728  P       p1491   String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"  P       p1491   String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3729  O       o1491   ext_rule p1491  O       o1491   ext_rule p1491
3730  T       t1491   o559 b561 b1474  T       t1491   o559 b561 b1474
# Line 3803  Line 3740 
3740  B       b1495   t1494  B       b1495   t1494
3741  T       t1495   o937 b1494 b4 b1495  T       t1495   o937 b1494 b4 b1495
3742  B       b1496   t1495  B       b1496   t1495
3743    T       t393    o b1496 b4
3744    B       b393    t393
3745    T       t399    o936 b1479 b393
3746    B       b399    t399
3747  B       b1497   t1474 v_3  B       b1497   t1474 v_3
3748  T       t1497   o711 b1497  T       t1497   o711 b1497
3749  S       s1497   t620 h h1454 h1465 h1475  S       s1497   t620 h h1454 h1465 h1475
# Line 3824  Line 3765 
3765  B       b1504   t1503  B       b1504   t1503
3766  T       t1504   o973 b1499 b4 b1504  T       t1504   o973 b1499 b4 b1504
3767  B       b1505   t1504  B       b1505   t1504
 T       t1505   o b1505 b4  
 B       b1506   t1505  
 T       t1506   o b1496 b1506  
 B       b1507   t1506  
 T       t1507   o936 b1479 b1507  
 B       b1508   t1507  
3768  P       p1508   String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"  P       p1508   String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3769  O       o1508   ext_rule p1508  O       o1508   ext_rule p1508
3770  T       t1508   o559 b560 b567  T       t1508   o559 b560 b567
# Line 3864  Line 3799 
3799  B       b1519   t1518  B       b1519   t1518
3800  T       t1519   o937 b1518 b4 b1519  T       t1519   o937 b1518 b4 b1519
3801  B       b1520   t1519  B       b1520   t1519
3802    T       t400    o b1520 b4
3803    B       b400    t400
3804    T       t406    o936 b1514 b400
3805    B       b406    t406
3806  B       b1521   t1509 v_5  B       b1521   t1509 v_5
3807  T       t1521   o711 b1521  T       t1521   o711 b1521
3808  S       s1521   t620 h h1454 h1465 h1475 h1492 h1510  S       s1521   t620 h h1454 h1465 h1475 h1492 h1510
# Line 3885  Line 3824 
3824  B       b1528   t1527  B       b1528   t1527
3825  T       t1528   o973 b1523 b4 b1528  T       t1528   o973 b1523 b4 b1528
3826  B       b1529   t1528  B       b1529   t1528
 T       t1529   o b1529 b4  
 B       b1530   t1529  
 T       t1530   o b1520 b1530  
 B       b1531   t1530  
 T       t1531   o936 b1514 b1531  
 B       b1532   t1531  
3827  P       p1532   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"  P       p1532   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3828  O       o1532   ext_rule p1532  O       o1532   ext_rule p1532
3829  T       t1532   o936 b1520 b4  T       t1532   o936 b1520 b4
3830  B       b1533   t1532  B       b1533   t1532
3831  T       t1533   o1532 b935 b1533 b4 b4  T       t1533   o1532 b935 b1533 b4 b4
3832  B       b1534   t1533  B       b1534   t1533
3833    T       t407    o b1534 b4
3834    B       b407    t407
3835  T       t1534   o936 b1529 b4  T       t1534   o936 b1529 b4
3836  B       b1535   t1534  B       b1535   t1534
3837  T       t1535   o1050 b935 b1535 b4 b4  T       t1535   o1050 b935 b1535 b4 b4
3838  B       b1536   t1535  B       b1536   t1535
3839  T       t1536   o b1536 b4  T       t1536   o b1536 b4
3840  B       b1537   t1536  B       b1537   t1536
3841  T       t1537   o b1534 b1537  T       t416    o1516 b935 b406 b407 b1537
3842  B       b1538   t1537  B       b416    t416
3843  T       t1538   o1516 b935 b1532 b1538 b4  T       t417    o b416 b4
3844  B       b1539   t1538  B       b417    t417
3845  T       t1539   o b1539 b4  T       t425    o1508 b935 b1516 b417 b4
3846  B       b1540   t1539  B       b425    t425
3847  T       t1540   o1508 b935 b1516 b1540 b4  T       t426    o b425 b4
3848  B       b1541   t1540  B       b426    t426
3849  T       t1541   o936 b1505 b4  T       t1541   o936 b1505 b4
3850  B       b1542   t1541  B       b1542   t1541
3851  T       t1542   o1050 b935 b1542 b4 b4  T       t1542   o1050 b935 b1542 b4 b4
3852  B       b1543   t1542  B       b1543   t1542
3853  T       t1543   o b1543 b4  T       t1543   o b1543 b4
3854  B       b1544   t1543  B       b1544   t1543
3855  T       t1544   o b1541 b1544  T       t434    o1491 b935 b399 b426 b1544
3856  B       b1545   t1544  B       b434    t434
3857  T       t1545   o1491 b935 b1508 b1545 b4  T       t435    o b434 b4
3858  B       b1546   t1545  B       b435    t435
3859  T       t1546   o936 b1488 b4  T       t1546   o936 b1488 b4
3860  B       b1547   t1546  B       b1547   t1546
3861  T       t1547   o1050 b935 b1547 b4 b4  T       t1547   o1050 b935 b1547 b4 b4
3862  B       b1548   t1547  B       b1548   t1547
3863  T       t1548   o b1548 b4  T       t1548   o b1548 b4
3864  B       b1549   t1548  B       b1549   t1548
3865  T       t1549   o b1546 b1549  T       t443    o1473 b935 b392 b435 b1549
3866  B       b1550   t1549  B       b443    t443
3867  T       t1550   o1473 b935 b1491 b1550 b4  T       t444    o b443 b4
3868  B       b1551   t1550  B       b444    t444
3869  T       t1551   o b1551 b4  T       t452    o b1473 b444
3870  B       b1552   t1551  B       b452    t452
 T       t1552   o b1473 b1552  
 B       b1553   t1552  
3871  S       s1553   t620 h  S       s1553   t620 h
3872  G       s1553   t1457  G       s1553   t1457
3873  B       b1554   s1553  B       b1554   s1553
# Line 4114  Line 4047 
4047  B       b1632   t1631  B       b1632   t1631
4048  T       t1632   o b1559 b1632  T       t1632   o b1559 b1632
4049  B       b1633   t1632  B       b1633   t1632
4050  T       t1633   o1445 b935 b1471 b1553 b1633  T       t453    o1445 b935 b1471 b452 b1633
4051  B       b1634   t1633  B       b453    t453
4052  T       t1634   o933 b1634  T       t461    o933 b453
4053  B       b1635   t1634  B       b461    t461
4054  P       p1635   Number 5861  P       p1635   Number 5861
4055  P       p1636   Number 5869  P       p1636   Number 5869
4056  O       o1636   resource_defs p1635 p1636 p264  O       o1636   resource_defs p1635 p1636 p264
# Line 4131  Line 4064 
4064  B       b1639   t1639  B       b1639   t1639
4065  T       t1640   o b1639 b4  T       t1640   o b1639 b4
4066  B       b1640   t1640  B       b1640   t1640
4067  T       t1641   o1432 b1434 b1445 b1635 b1640  T       t462    o1432 b1434 b1445 b461 b1640
4068  B       b1641   t1641  B       b462    t462
4069  T       t1642   o1431 b1641  T       t470    o1431 b462
4070  B       b1642   t1642  B       b470    t470
4071  P       p1642   Number 6266  P       p1642   Number 6266
4072  P       p1643   Number 6335  P       p1643   Number 6335
4073  O       o1643   location p1642 p1643  O       o1643   location p1642 p1643
# Line 4536  Line 4469 
4469  B       b1806   t1805  B       b1806   t1805
4470  T       t1806   o937 b1806 b4 b1782  T       t1806   o937 b1806 b4 b1782
4471  B       b1807   t1806  B       b1807   t1806
4472  B       b1808   t1745 v  T       t471    o b1807 b4
4473  T       t1808   o711 b1808  B       b471    t471
4474  S       s1808   t620 h h1736 h1746 h1748  T       t479    o b1804 b471
4475  G       s1808   t1808  B       b479    t479
4476  B       b1809   s1808  T       t480    o b1801 b479
4477  T       t1809   o938 b1809 b1769  B       b480    t480
4478  B       b1810   t1809  T       t486    o936 b1777 b480
4479  B       b1811   t1746 v  B       b486    t486
 T       t1811   o976 b1811  
 S       s1811   t620 h h1736 h1746 h1748  
 G       s1811   t1811  
 B       b1812   s1811  
 T       t1812   o938 b1812 b1769  
 B       b1813   t1812  
 T       t1813   o973 b1813 b983 b1782  
 B       b1814   t1813  
 T       t1814   o2 b1814  
 B       b1815   t1814  
 T       t1815   o973 b1810 b4 b1815  
 B       b1816   t1815  
 T       t1816   o b1816 b4  
 B       b1817   t1816  
 T       t1817   o b1807 b1817  
 B       b1818   t1817  
 T       t1818   o b1804 b1818  
 B       b1819   t1818  
 T       t1819   o b1801 b1819  
 B       b1820   t1819  
 T       t1820   o936 b1777 b1820  
 B       b1821   t1820  
4480  T       t1821   o1085 b1801  T       t1821   o1085 b1801
4481  B       b1822   t1821  B       b1822   t1821
4482  T       t1822   o1085 b1804  T       t1822   o1085 b1804
4483  B       b1823   t1822  B       b1823   t1822
4484  T       t1823   o1085 b1807  T       t1823   o1085 b1807
4485  B       b1824   t1823  B       b1824   t1823
4486  T       t1824   o1085 b1816  T       t487    o b1824 b4
4487  B       b1825   t1824  B       b487    t487
4488  T       t1825   o b1825 b4  T       t493    o b1823 b487
4489  B       b1826   t1825  B       b493    t493
4490  T       t1826   o b1824 b1826  T       t494    o b1822 b493
4491  B       b1827   t1826  B       b494    t494
4492  T       t1827   o b1823 b1827  T       t500    o1788 b935 b486 b494 b4
4493  B       b1828   t1827  B       b500    t500
4494  T       t1828   o b1822 b1828  T       t501    o b500 b4
4495  B       b1829   t1828  B       b501    t501
4496  T       t1829   o1788 b935 b1821 b1829 b4  T       t508    o b500 b501
4497  B       b1830   t1829  B       b508    t508
4498  T       t1830   o b1830 b4  T       t509    o b1788 b508
4499  B       b1831   t1830  B       b509    t509
4500  T       t1831   o b1830 b1831  T       t516    o b1779 b509
4501  B       b1832   t1831  B       b516    t516
4502  T       t1832   o b1788 b1832  T       t517    o1740 b935 b1764 b1767 b516
4503  B       b1833   t1832  B       b517    t517
4504  T       t1833   o b1779 b1833  T       t524    o933 b517
4505  B       b1834   t1833  B       b524    t524
 T       t1834   o1740 b935 b1764 b1767 b1834  
 B       b1835   t1834  
 T       t1835   o933 b1835  
 B       b1836   t1835  
4506  P       p1836   Number 6451  P       p1836   Number 6451
4507  P       p1837   Number 6459  P       p1837   Number 6459
4508  O       o1837   resource_defs p1836 p1837 p264  O       o1837   resource_defs p1836 p1837 p264
# Line 4609  Line 4516 
4516  B       b1840   t1840  B       b1840   t1840
4517  T       t1841   o b1840 b4  T       t1841   o b1840 b4
4518  B       b1841   t1841  B       b1841   t1841
4519  T       t1842   o1725 b618 b1740 b1836 b1841  T       t525    o1725 b618 b1740 b524 b1841
4520  B       b1842   t1842  B       b525    t525
4521  T       t1843   o1724 b1842  T       t531    o1724 b525
4522  B       b1843   t1843  B       b531    t531
4523  P       p1843   Number 6981  P       p1843   Number 6981
4524  P       p1844   Number 7305  P       p1844   Number 7305
4525  O       o1844   location p1843 p1844  O       o1844   location p1843 p1844
# Line 4702  Line 4609 
4609  B       b1877   t1877  B       b1877   t1877
4610  T       t1878   o937 b1877 b4 b1872  T       t1878   o937 b1877 b4 b1872
4611  B       b1878   t1878  B       b1878   t1878
4612    T       t532    o b1878 b4
4613    B       b532    t532
4614    T       t538    o b1875 b532
4615    B       b538    t538
4616    T       t539    o936 b1865 b538
4617    B       b539    t539
4618  B       b1879   t1845 v_1  B       b1879   t1845 v_1
4619  T       t1879   o711 b1879  T       t1879   o711 b1879
4620  S       s1879   t620 h h1846 h1848 h1862  S       s1879   t620 h h1846 h1848 h1862
# Line 4723  Line 4636 
4636  B       b1886   t1885  B       b1886   t1885
4637  T       t1886   o973 b1881 b4 b1886  T       t1886   o973 b1881 b4 b1886
4638  B       b1887   t1886  B       b1887   t1886
 T       t1887   o b1887 b4  
 B       b1888   t1887  
 T       t1888   o b1878 b1888  
 B       b1889   t1888  
 T       t1889   o b1875 b1889  
 B       b1890   t1889  
 T       t1890   o936 b1865 b1890  
 B       b1891   t1890  
4639  P       p1891   String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"  P       p1891   String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4640  O       o1891   ext_rule p1891  O       o1891   ext_rule p1891
4641  T       t1891   o936 b1875 b4  T       t1891   o936 b1875 b4
# Line 4743  Line 4648 
4648  B       b1894   t1893  B       b1894   t1893
4649  T       t1894   o1893 b935 b1894 b4 b4  T       t1894   o1893 b935 b1894 b4 b4
4650  B       b1895   t1894  B       b1895   t1894
4651    T       t545    o b1895 b4
4652    B       b545    t545
4653    T       t546    o b1893 b545
4654    B       b546    t546
4655  T       t1895   o936 b1887 b4  T       t1895   o936 b1887 b4
4656  B       b1896   t1895  B       b1896   t1895
4657  T       t1896   o1071 b935 b1896 b4 b4  T       t1896   o1071 b935 b1896 b4 b4
4658  B       b1897   t1896  B       b1897   t1896
4659  T       t1897   o b1897 b4  T       t1897   o b1897 b4
4660  B       b1898   t1897  B       b1898   t1897
4661  T       t1898   o b1895 b1898  T       t552    o1867 b935 b539 b546 b1898
4662  B       b1899   t1898  B       b552    t552
4663  T       t1899   o b1893 b1899  T       t553    o b552 b4
4664  B       b1900   t1899  B       b553    t553
4665  T       t1900   o1867 b935 b1891 b1900 b4  T       t557    o1854 b935 b1867 b553 b4
4666  B       b1901   t1900  B       b557    t557
4667  T       t1901   o b1901 b4  T       t558    o933 b557
4668  B       b1902   t1901  B       b558    t558
 T       t1902   o1854 b935 b1867 b1902 b4  
 B       b1903   t1902  
 T       t1903   o933 b1903  
 B       b1904   t1903  
4669  P       p1904   Number 7007  P       p1904   Number 7007
4670  P       p1905   Number 7015  P       p1905   Number 7015
4671  O       o1905   resource_defs p1904 p1905 p264  O       o1905   resource_defs p1904 p1905 p264
# Line 4774  Line 4679 
4679  B       b1908   t1908  B       b1908   t1908
4680  T       t1909   o b1908 b4  T       t1909   o b1908 b4
4681  B       b1909   t1909  B       b1909   t1909
4682  T       t1910   o1845 b618 b1854 b1904 b1909  T       t559    o1845 b618 b1854 b558 b1909
4683  B       b1910   t1910  B       b559    t559
4684  T       t1911   o1844 b1910  T       t565    o1844 b559
4685  B       b1911   t1911  B       b565    t565
4686  P       p1911   Number 7356  P       p1911   Number 7356
4687  P       p1912   Number 7775  P       p1912   Number 7775
4688  O       o1912   location p1911 p1912  O       o1912   location p1911 p1912
# Line 4990  Line 4895 
4895  B       b1995   t1994  B       b1995   t1994
4896  T       t1995   o937 b1994 b4 b1995  T       t1995   o937 b1994 b4 b1995
4897  B       b1996   t1995  B       b1996   t1995
4898    T       t566    o b1996 b4
4899    B       b566    t566
4900    T       t570    o936 b1985 b566
4901    B       b570    t570
4902  B       b1997   t1933 v_1  B       b1997   t1933 v_1
4903  T       t1997   o711 b1997  T       t1997   o711 b1997
4904  S       s1997   t620 h h1952 h1953 h1954 h1982  S       s1997   t620 h h1952 h1953 h1954 h1982
# Line 5011  Line 4920 
4920  B       b2004   t2003  B       b2004   t2003
4921  T       t2004   o973 b1999 b4 b2004  T       t2004   o973 b1999 b4 b2004
4922  B       b2005   t2004  B       b2005   t2004
 T       t2005   o b2005 b4  
 B       b2006   t2005  
 T       t2006   o b1996 b2006  
 B       b2007   t2006  
 T       t2007   o936 b1985 b2007  
 B       b2008   t2007  
4923  P       p2008   String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"  P       p2008   String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
4924  O       o2008   ext_rule p2008  O       o2008   ext_rule p2008
4925  T       t2008   o559 b567 b1920  T       t2008   o559 b567 b1920
# Line 5032  Line 4935 
4935  B       b2012   t2011  B       b2012   t2011
4936  T       t2012   o937 b2011 b4 b2012  T       t2012   o937 b2011 b4 b2012
4937  B       b2013   t2012  B       b2013   t2012
4938    T       t571    o b2013 b4
4939    B       b571    t571
4940    T       t572    o936 b1996 b571
4941    B       b572    t572
4942  B       b2014   t1933 v_2  B       b2014   t1933 v_2
4943  T       t2014   o711 b2014  T       t2014   o711 b2014
4944  S       s2014   t620 h h1952 h1953 h1954 h1982 h1992  S       s2014   t620 h h1952 h1953 h1954 h1982 h1992
# Line 5055  Line 4962 
4962  B       b2022   t2021  B       b2022   t2021
4963  T       t2022   o973 b2016 b4 b2022  T       t2022   o973 b2016 b4 b2022
4964  B       b2023   t2022  B       b2023   t2022
 T       t2023   o b2023 b4  
 B       b2024   t2023  
 T       t2024   o b2013 b2024  
 B       b2025   t2024  
 T       t2025   o936 b1996 b2025  
 B       b2026   t2025  
4965  P       p2026   String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"  P       p2026   String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
4966  O       o2026   ext_rule p2026  O       o2026   ext_rule p2026
4967  H       h2026   v_3 t1934  H       h2026   v_3 t1934
# Line 5073  Line 4974 
4974  B       b2029   t2028  B       b2029   t2028
4975  T       t2029   o937 b2028 b4 b2029  T       t2029   o937 b2028 b4 b2029
4976  B       b2030   t2029  B       b2030   t2029
4977    T       t577    o b2030 b4
4978    B       b577    t577
4979    T       t578    o936 b2013 b577
4980    B       b578    t578
4981  B       b2031   t1933 v_3  B       b2031   t1933 v_3
4982  T       t2031   o711 b2031  T       t2031   o711 b2031
4983  S       s2031   t620 h h1952 h1953 h1954 h1982 h1992 h2009  S       s2031   t620 h h1952 h1953 h1954 h1982 h1992 h2009
# Line 5094  Line 4999 
4999  B       b2038   t2037  B       b2038   t2037
5000  T       t2038   o973 b2033 b4 b2038  T       t2038   o973 b2033 b4 b2038
5001  B       b2039   t2038  B       b2039   t2038
 T       t2039   o b2039 b4  
 B       b2040   t2039  
 T       t2040   o b2030 b2040  
 B       b2041   t2040  
 T       t2041   o936 b2013 b2041  
 B       b2042   t2041  
5002  P       p2042   String "rwh unfold_equal 8 thenT autoT"  P       p2042   String "rwh unfold_equal 8 thenT autoT"
5003  O       o2042   ext_rule p2042  O       o2042   ext_rule p2042
5004  T       t2042   o936 b2030 b4  T       t2042   o936 b2030 b4
5005  B       b2043   t2042  B       b2043   t2042
5006  T       t2043   o2042 b935 b2043 b4 b4  T       t2043   o2042 b935 b2043 b4 b4
5007  B       b2044   t2043  B       b2044   t2043
5008    T       t586    o b2044 b4
5009    B       b586    t586
5010  T       t2044   o936 b2039 b4  T       t2044   o936 b2039 b4
5011  B       b2045   t2044  B       b2045   t2044
5012  T       t2045   o1071 b935 b2045 b4 b4  T       t2045   o1071 b935 b2045 b4 b4
5013  B       b2046   t2045  B       b2046   t2045
5014  T       t2046   o b2046 b4  T       t2046   o b2046 b4
5015  B       b2047   t2046  B       b2047   t2046
5016  T       t2047   o b2044 b2047  T       t587    o2026 b935 b578 b586 b2047
5017  B       b2048   t2047  B       b587    t587
5018  T       t2048   o2026 b935 b2042 b2048 b4  T       t593    o b587 b4
5019  B       b2049   t2048  B       b593    t593
5020  T       t2049   o936 b2023 b4  T       t2049   o936 b2023 b4
5021  B       b2050   t2049  B       b2050   t2049
5022  T       t2050   o1071 b935 b2050 b4 b4  T       t2050   o1071 b935 b2050 b4 b4
5023  B       b2051   t2050  B       b2051   t2050
5024  T       t2051   o b2051 b4  T       t2051   o b2051 b4
5025  B       b2052   t2051  B       b2052   t2051
5026  T       t2052   o b2049 b2052  T       t594    o2008 b935 b572 b593 b2052
5027  B       b2053   t2052  B       b594    t594
5028  T       t2053   o2008 b935 b2026 b2053 b4  T       t607    o b594 b4
5029  B       b2054   t2053  B       b607    t607
5030  T       t2054   o936 b2005 b4  T       t2054   o936 b2005 b4
5031  B       b2055   t2054  B       b2055   t2054
5032  T       t2055   o1071 b935 b2055 b4 b4  T       t2055   o1071 b935 b2055 b4 b4
5033  B       b2056   t2055  B       b2056   t2055
 T       t2056   o b2056 b4  
 B       b2057   t2056  
 T       t2057   o b2054 b2057  
 B       b2058   t2057  
5034  T       t2058   o738 b1954 b1992  T       t2058   o738 b1954 b1992
5035  S       s2058   t620 h h1952 h1953 h1954 h1982  S       s2058   t620 h h1952 h1953 h1954 h1982
5036  G       s2058   t2058  G       s2058   t2058
# Line 5150  Line 5047 
5047  O       o2063   ext_rule p2063  O       o2063   ext_rule p2063
5048  T       t2063   o973 b2002 b4 b1995  T       t2063   o973 b2002 b4 b1995
5049  B       b2064   t2063  B       b2064   t2063
5050    T       t615    o936 b2064 b4
5051    B       b615    t615
5052  H       h2064   x_1 t1344  H       h2064   x_1 t1344
5053  H       h2065   y_2 t638  H       h2065   y_2 t638
5054  T       t2065   o620 b1933  T       t2065   o620 b1933
# Line 5279  Line 5178 
5178  B       b2119   t2118  B       b2119   t2118
5179  T       t2119   o973 b2068 b4 b2119  T       t2119   o973 b2068 b4 b2119
5180  B       b2120   t2119  B       b2120   t2119
 T       t2120   o b2120 b4  
 B       b2121   t2120  
 T       t2121   o936 b2064 b2121  
 B       b2122   t2121  
5181  T       t2122   o936 b2120 b4  T       t2122   o936 b2120 b4
5182  B       b2123   t2122  B       b2123   t2122
5183  T       t2123   o1071 b935 b2123 b4 b4  T       t2123   o1071 b935 b2123 b4 b4
5184  B       b2124   t2123  B       b2124   t2123
5185  T       t2124   o b2124 b4  T       t2124   o b2124 b4
5186  B       b2125   t2124  B       b2125   t2124
5187  T       t2125   o2063 b935 b2122 b2125 b4  T       t616    o2063 b935 b615 b4 b2125
5188  B       b2126   t2125  B       b616    t616
5189  T       t2126   o b2126 b4  T       t624    o b616 b4
5190  B       b2127   t2126  B       b624    t624
5191  T       t2127   o b2063 b2127  T       t625    o b2063 b624
5192  B       b2128   t2127  B       b625    t625
5193  T       t2128   o1990 b935 b2008 b2058 b2128  T       t633    o b2056 b625
5194  B       b2129   t2128  B       b633    t633
5195  T       t2129   o b2129 b4  T       t634    o1990 b935 b570 b607 b633
5196  B       b2130   t2129  B       b634    t634
5197  T       t2130   o b1990 b2130  T       t635    o b634 b4
5198  B       b2131   t2130  B       b635    t635
5199  T       t2131   o1942 b935 b1988 b2131 b4  T       t646    o b1990 b635
5200  B       b2132   t2131  B       b646    t646
5201  T       t2132   o933 b2132  T       t653    o1942 b935 b1988 b646 b4
5202  B       b2133   t2132  B       b653    t653
5203    T       t654    o933 b653
5204    B       b654    t654
5205  P       p2133   Number 7383  P       p2133   Number 7383
5206  P       p2134   Number 7391  P       p2134   Number 7391
5207  O       o2134   resource_defs p2133 p2134 p264  O       o2134   resource_defs p2133 p2134 p264
# Line 5318  Line 5215 
5215  B       b2137   t2137  B       b2137   t2137
5216  T       t2138   o b2137 b4  T       t2138   o b2137 b4
5217  B       b2138   t2138  B       b2138   t2138
5218  T       t2139   o1913 b618 b1942 b2133 b2138  T       t665    o1913 b618 b1942 b654 b2138
5219  B       b2139   t2139  B       b665    t665
5220  T       t2140   o1912 b2139  T       t672    o1912 b665
5221  B       b2140   t2140  B       b672    t672
5222  P       p2140   Number 7826  P       p2140   Number 7826
5223  P       p2141   Number 8245  P       p2141   Number 8245
5224  O       o2141   location p2140 p2141  O       o2141   location p2140 p2141
# Line 5482  Line 5379 
5379  B       b2203   t2202  B       b2203   t2202
5380  T       t2203   o937 b2202 b4 b2203  T       t2203   o937 b2202 b4 b2203
5381  B       b2204   t2203  B       b2204   t2203
5382    T       t673    o b2204 b4
5383    B       b673    t673
5384    T       t687    o936 b2193 b673
5385    B       b687    t687
5386  B       b2205   t2151 v_2  B       b2205   t2151 v_2
5387  T       t2205   o711 b2205  T       t2205   o711 b2205
5388  S       s2205   t620 h h2169 h2186  S       s2205   t620 h h2169 h2186
# Line 5503  Line 5404 
5404  B       b2212   t2211  B       b2212   t2211
5405  T       t2212   o973 b2207 b4 b2212  T       t2212   o973 b2207 b4 b2212
5406  B       b2213   t2212  B       b2213   t2212
 T       t2213   o b2213 b4  
 B       b2214   t2213  
 T       t2214   o b2204 b2214  
 B       b2215   t2214  
 T       t2215   o936 b2193 b2215  
 B       b2216   t2215  
5407  P       p2216   String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"  P       p2216   String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5408  O       o2216   ext_rule p2216  O       o2216   ext_rule p2216
5409  T       t2216   o559 b2143 b567  T       t2216   o559 b2143 b567
# Line 5524  Line 5419 
5419  B       b2220   t2219  B       b2220   t2219
5420  T       t2220   o937 b2219 b4 b2220  T       t2220   o937 b2219 b4 b2220
5421  B       b2221   t2220  B       b2221   t2220
5422    T       t694    o b2221 b4
5423    B       b694    t694
5424    T       t703    o936 b2204 b694
5425    B       b703    t703
5426  B       b2222   t2151 v_3  B       b2222   t2151 v_3
5427  T       t2222   o711 b2222  T       t2222   o711 b2222
5428  S       s2222   t620 h h2169 h2186 h2200  S       s2222   t620 h h2169 h2186 h2200
# Line 5547  Line 5446 
5446  B       b2230   t2229  B       b2230   t2229
5447  T       t2230   o973 b2224 b4 b2230  T       t2230   o973 b2224 b4 b2230
5448  B       b2231   t2230  B       b2231   t2230
 T       t2231   o b2231 b4  
 B       b2232   t2231  
 T       t2232   o b2221 b2232  
 B       b2233   t2232  
 T       t2233   o936 b2204 b2233  
 B       b2234   t2233  
5449  P       p2234   String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"  P       p2234   String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5450  O       o2234   ext_rule p2234  O       o2234   ext_rule p2234
5451    T       t717    o936 b2221 b4
5452    B       b717    t717
5453  T       t2234   o620 b2217  T       t2234   o620 b2217
5454  H       h2234   y_2 t2234  H       h2234   y_2 t2234
5455  T       t2235   o620 b2151  T       t2235   o620 b2151
# Line 5617  Line 5512 
5512  B       b2259   t2258  B       b2259   t2258
5513  T       t2259   o973 b2237 b4 b2259  T       t2259   o973 b2237 b4 b2259
5514  B       b2260   t2259  B       b2260   t2259
 T       t2260   o b2260 b4  
 B       b2261   t2260  
 T       t2261   o936 b2221 b2261  
 B       b2262   t2261  
5515  T       t2262   o936 b2260 b4  T       t2262   o936 b2260 b4
5516  B       b2263   t2262  B       b2263   t2262
5517  T       t2263   o1071 b935 b2263 b4 b4  T       t2263   o1071 b935 b2263 b4 b4
5518  B       b2264   t2263  B       b2264   t2263
5519  T       t2264   o b2264 b4  T       t2264   o b2264 b4
5520  B       b2265   t2264  B       b2265   t2264
5521  T       t2265   o2234 b935 b2262 b2265 b4  T       t724    o2234 b935 b717 b4 b2265
5522  B       b2266   t2265  B       b724    t724
5523    T       t729    o b724 b4
5524    B       b729    t729
5525  T       t2266   o936 b2231 b4  T       t2266   o936 b2231 b4
5526  B       b2267   t2266  B       b2267   t2266
5527  T       t2267   o1071 b935 b2267 b4 b4  T       t2267   o1071 b935 b2267 b4 b4
5528  B       b2268   t2267  B       b2268   t2267
5529  T       t2268   o b2268 b4  T       t2268   o b2268 b4
5530  B       b2269   t2268  B       b2269   t2268
5531  T       t2269   o b2266 b2269  T       t736    o2216 b935 b703 b729 b2269
5532  B       b2270   t2269  B       b736    t736
5533  T       t2270   o2216 b935 b2234 b2270 b4  T       t749    o b736 b4
5534  B       b2271   t2270  B       b749    t749
5535  T       t2271   o936 b2213 b4  T       t2271   o936 b2213 b4
5536  B       b2272   t2271  B       b2272   t2271
5537  T       t2272   o1071 b935 b2272 b4 b4  T       t2272   o1071 b935 b2272 b4 b4
5538  B       b2273   t2272  B       b2273   t2272
5539  T       t2273   o b2273 b4  T       t2273   o b2273 b4
5540  B       b2274   t2273  B       b2274   t2273
5541  T       t2274   o b2271 b2274  T       t756    o2198 b935 b687 b749 b2274
5542  B       b2275   t2274  B       b756    t756
5543  T       t2275   o2198 b935 b2216 b2275 b4  T       t765    o b756 b4
5544  B       b2276   t2275  B       b765    t765
5545  T       t2276   o b2276 b4  T       t772    o b2198 b765
5546  B       b2277   t2276  B       b772    t772
5547  T       t2277   o b2198 b2277  T       t775    o2160 b935 b2196 b772 b4
5548  B       b2278   t2277  B       b775    t775
5549  T       t2278   o2160 b935 b2196 b2278 b4  T       t782    o933 b775
5550  B       b2279   t2278  B       b782    t782
 T       t2279   o933 b2279  
 B       b2280   t2279  
5551  P       p2280   Number 7853  P       p2280   Number 7853
5552  P       p2281   Number 7861  P       p2281   Number 7861
5553  O       o2281   resource_defs p2280 p2281 p264  O       o2281   resource_defs p2280 p2281 p264
# Line 5670  Line 5561 
5561  B       b2284   t2284  B       b2284   t2284
5562  T       t2285   o b2284 b4  T       t2285   o b2284 b4
5563  B       b2285   t2285  B       b2285   t2285
5564  T       t2286   o2142 b618 b2160 b2280 b2285  T       t785    o2142 b618 b2160 b782 b2285
5565  B       b2286   t2286  B       b785    t785
5566  T       t2287   o2141 b2286  T       t792    o2141 b785
5567  B       b2287   t2287  B       b792    t792
5568  P       p2287   Number 8273  P       p2287   Number 8273
5569  P       p2288   Number 8568  P       p2288   Number 8568
5570  O       o2288   location p2287 p2288  O       o2288   location p2287 p2288
# Line 5701  Line 5592 
5592  B       b2297   t2297  B       b2297   t2297
5593  T       t2298   o635 b1916 b2297  T       t2298   o635 b1916 b2297
5594  B       b2298   t2298  B       b2298   t2298
5595  P       p2298   String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >> thenAT autoT"  P       p794    String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >>"
5596  O       o2298   ext_rule p2298  O       o794    ext_rule p794
5597  T       t2299   o b1925 b4  T       t2299   o b1925 b4
5598  B       b2299   t2299  B       b2299   t2299
5599  T       t2300   o b1923 b2299  T       t2300   o b1923 b2299
# Line 5763  Line 5654 
5654  B       b2322   t2321  B       b2322   t2321
5655  T       t2322   o937 b2322 b4 b2319  T       t2322   o937 b2322 b4 b2319
5656  B       b2323   t2322  B       b2323   t2322
5657  B       b2324   t2306 v  T       t800    o b2323 b4
5658  T       t2324   o711 b2324  B       b800    t800
5659  S       s2324   t620 h  T       t807    o b2320 b800
5660  G       s2324   t2324  B       b807    t807
5661  B       b2325   s2324  T       t813    o936 b2310 b807
5662  T       t2325   o938 b2325 b2302  B       b813    t813
 B       b2326   t2325  
5663  P       p2326   Var v  P       p2326   Var v
5664  O       o2326   var p2326  O       o2326   var p2326
5665  T       t2326   o2326  T       t2326   o2326
5666  B       b2327   t2326  B       b2327   t2326
 T       t2327   o738 b2327 b2306  
 B       b2328   t2327 v  
 T       t2328   o976 b2328  
 S       s2328   t620 h  
 G       s2328   t2328  
 B       b2329   s2328  
 T       t2329   o938 b2329 b2302  
 B       b2330   t2329  
 T       t2330   o973 b2330 b983 b2319  
 B       b2331   t2330  
 T       t2331   o2 b2331  
 B       b2332   t2331  
 T       t2332   o973 b2326 b4 b2332  
 B       b2333   t2332  
 T       t2333   o b2333 b4  
 B       b2334   t2333  
 T       t2334   o b2323 b2334  
 B       b2335   t2334  
 T       t2335   o b2320 b2335  
 B       b2336   t2335  
 T       t2336   o936 b2310 b2336  
 B       b2337   t2336  
5667  T       t2337   o936 b2320 b4  T       t2337   o936 b2320 b4
5668  B       b2338   t2337  B       b2338   t2337
5669  T       t2338   o990 b935 b2338 b4 b4  T       t2338   o990 b935 b2338 b4 b4
# Line 5824  Line 5692 
5692  B       b2347   t2346  B       b2347   t2346
5693  T       t2347   o937 b2347 b4 b2344  T       t2347   o937 b2347 b4 b2344
5694  B       b2348   t2347  B       b2348   t2347
5695  T       t2348   o973 b2330 b983 b2344  T       t820    o b2348 b4
5696  B       b2349   t2348  B       b820    t820
5697  T       t2349   o2 b2349  T       t821    o b2345 b820
5698  B       b2350   t2349  B       b821    t821
5699  T       t2350   o973 b2326 b4 b2350  T       t822    o936 b2323 b821
5700  B       b2351   t2350  B       b822    t822
 T       t2351   o b2351 b4  
 B       b2352   t2351  
 T       t2352   o b2348 b2352  
 B       b2353   t2352  
 T       t2353   o b2345 b2353  
 B       b2354   t2353  
 T       t2354   o936 b2323 b2354  
 B       b2355   t2354  
5701  P       p2355   String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"  P       p2355   String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5702  O       o2355   ext_rule p2355  O       o2355   ext_rule p2355
5703  T       t2355   o559 b1991 b1917  T       t2355   o559 b1991 b1917
# Line 6130  Line 5990 
5990  B       b2479   t2478  B       b2479   t2478
5991  T       t2479   o990 b935 b2479 b4 b4  T       t2479   o990 b935 b2479 b4 b4
5992  B       b2480   t2479  B       b2480   t2479
5993  T       t2480   o936 b2351 b4  T       t825    o b2480 b4
5994  B       b2481   t2480  B       b825    t825
5995  T       t2481   o1050 b935 b2481 b4 b4  T       t826    o b2478 b825
5996  B       b2482   t2481  B       b826    t826
5997  T       t2482   o b2482 b4  T       t827    o2339 b935 b822 b826 b4
5998  B       b2483   t2482  B       b827    t827
5999  T       t2483   o b2480 b2483  T       t828    o b827 b4
6000  B       b2484   t2483  B       b828    t828
6001  T       t2484   o b2478 b2484  T       t829    o b2339 b828
6002  B       b2485   t2484  B       b829    t829
6003  T       t2485   o2339 b935 b2355 b2485 b4  T       t830    o2316 b935 b813 b829 b4
6004  B       b2486   t2485  B       b830    t830
 T       t2486   o738 b2306 b2306  
 S       s2486   t620 h h1344 h1224 h1345  
 G       s2486   t2486  
 B       b2487   s2486  
 T       t2487   o938 b2487 b2302  
 B       b2488   t2487  
 B       b2489   t2486  
 T       t2489   o1177 b1347 b2489  
 S       s2489   t620 h h1344 h1224  
 G       s2489   t2489  
 B       b2490   s2489  
 T       t2490   o938 b2490 b2302  
 B       b2491   t2490  
 B       b2492   t2489 s2  
 T       t2492   o1185 b1186 b2492  
 S       s2492   t620 h h1344  
 G       s2492   t2492  
 B       b2493   s2492  
 T       t2493   o938 b2493 b2302  
 B       b2494   t2493  
 B       b2495   t2492 s1  
 T       t2495   o1185 b1186 b2495  
 S       s2495   t620 h  
 G       s2495   t2495  
 B       b2496   s2495  
 T       t2496   o938 b2496 b2302  
 B       b2497   t2496  
 T       t2497   o2 b2333  
 B       b2498   t2497  
 T       t2498   o973 b2497 b983 b2498  
 B       b2499   t2498  
 T       t2499   o2 b2499  
 B       b2500   t2499  
 T       t2500   o937 b2494 b983 b2500  
 B       b2501   t2500  
 T       t2501   o2 b2501  
 B       b2502   t2501  
 T       t2502   o937 b2491 b983 b2502  
 B       b2503   t2502  
 T       t2503   o2 b2503  
 B       b2504   t2503  
 T       t2504   o937 b2488 b4 b2504  
 B       b2505   t2504  
 T       t2505   o b2505 b4  
 B       b2506   t2505  
 T       t2506   o936 b2333 b2506  
 B       b2507   t2506  
 P       p2507   String "rwh unfold_equal 0 thenT autoT"  
 O       o2507   ext_rule p2507  
 T       t2507   o936 b2505 b4  
 B       b2508   t2507  
 T       t2508   o2507 b935 b2508 b4 b4  
 B       b2509   t2508  
 T       t2509   o b2509 b4  
 B       b2510   t2509  
 T       t2510   o1071 b935 b2507 b2510 b4  
 B       b2511   t2510  
 T       t2511   o b2511 b4  
 B       b2512   t2511  
 T       t2512   o b2486 b2512  
 B       b2513   t2512  
 T       t2513   o b2339 b2513  
 B       b2514   t2513  
 T       t2514   o2316 b935 b2337 b2514 b4  
 B       b2515   t2514  
6005  P       p2515   String "groupCancelRightT << op{'a; 'b} >> thenT autoT"  P       p2515   String "groupCancelRightT << op{'a; 'b} >> thenT autoT"
6006  O       o2515   ext_rule p2515  O       o2515   ext_rule p2515
6007  T       t2515   o936 b2313 b4  T       t2515   o936 b2313 b4
# Line 6215  Line 6010 
6010  B       b2517   t2516  B       b2517   t2516
6011  T       t2517   o b2517 b4  T       t2517   o b2517 b4
6012  B       b2518   t2517  B       b2518   t2517
6013  T       t2518   o b2515 b2518  T       t833    o b830 b2518
6014  B       b2519   t2518  B       b833    t833
6015  T       t2519   o2298 b935 b2316 b2519 b4  T       t834    o794 b935 b2316 b833 b4
6016  B       b2520   t2519  B       b834    t834
6017  T       t2520   o933 b2520  T       t835    o933 b834
6018  B       b2521   t2520  B       b835    t835
6019  P       p2521   Number 8301  P       p2521   Number 8301
6020  P       p2522   Number 8309  P       p2522   Number 8309
6021  O       o2522   resource_defs p2521 p2522 p264  O       o2522   resource_defs p2521 p2522 p264
# Line 6234  Line 6029 
6029  B       b2525   t2525  B       b2525   t2525
6030  T       t2526   o b2525 b4  T       t2526   o b2525 b4
6031  B       b2526   t2526  B       b2526   t2526
6032  T       t2527   o2289 b618 b2298 b2521 b2526  T       t856    o2289 b618 b2298 b835 b2526
6033  B       b2527   t2527  B       b856    t856
6034  T       t2528   o2288 b2527  T       t862    o2288 b856
6035  B       b2528   t2528  B       b862    t862
6036  O       o2528   location p p  O       o2528   location p p
6037  NSummary!id     id2528  id Summary  NSummary!id     id2528  id Summary
6038  P       p2528   Number 646427455  P       p2528   Number 646427455
# Line 6248  Line 6043 
6043  B       b2530   t2530  B       b2530   t2530
6044  T       t2531   o b2530 b4  T       t2531   o b2530 b4
6045  B       b2531   t2531  B       b2531   t2531
6046  T       t2532   o b2528 b2531  T       t869    o b862 b2531
6047  B       b2532   t2532  B       b869    t869
6048  T       t2533   o b2287 b2532  T       t874    o b792 b869
6049  B       b2533   t2533  B       b874    t874
6050  T       t2534   o b2140 b2533  T       t881    o b672 b874
6051  B       b2534   t2534  B       b881    t881
6052  T       t2535   o b1911 b2534  T       t885    o b565 b881
6053  B       b2535   t2535  B       b885    t885
6054  T       t2536   o b1843 b2535  T       t892    o b531 b885
6055  B       b2536   t2536  B       b892    t892
6056  T       t2537   o b1723 b2536  T       t898    o b1723 b892
6057  B       b2537   t2537  B       b898    t898
6058  T       t2538   o b1683 b2537  T       t905    o b1683 b898
6059  B       b2538   t2538  B       b905    t905
6060  T       t2539   o b1642 b2538  T       t911    o b470 b905
6061  B       b2539   t2539  B       b911    t911
6062  T       t2540   o b1430 b2539  T       t918    o b385 b911
6063  B       b2540   t2540  B       b918    t918
6064  T       t2541   o b917 b2540  T       t919    o b917 b918
6065  B       b2541   t2541  B       b919    t919
6066  T       t2542   o b904 b2541  T       t934    o b904 b919
6067  B       b2542   t2542  B       b934    t934
6068  T       t2543   o b891 b2542  T       t936    o b891 b934
6069  B       b2543   t2543  B       b936    t936
6070  T       t2544   o b880 b2543  T       t937    o b880 b936
6071  B       b2544   t2544  B       b937    t937
6072  T       t2545   o b868 b2544  T       t957    o b868 b937
6073  B       b2545   t2545  B       b1097   t957
6074  T       t2546   o b855 b2545  T       t1097   o b855 b1097
6075  B       b2546   t2546  B       b1098   t1097
6076  T       t2547   o b819 b2546  T       t1098   o b819 b1098
6077  B       b2547   t2547  B       b1099   t1098
6078  T       t2548   o b806 b2547  T       t1099   o b806 b1099
6079  B       b2548   t2548  B       b1172   t1099
6080  T       t2549   o b791 b2548  T       t1178   o b791 b1172
6081  B       b2549   t2549  B       b1225   t1178
6082  T       t2550   o b781 b2549  T       t1230   o b781 b1225
6083  B       b2550   t2550  B       b1265   t1230
6084  T       t2551   o b771 b2550  T       t1270   o b771 b1265
6085  B       b2551   t2551  B       b1424   t1270
6086  T       t2552   o b755 b2551  T       t1424   o b755 b1424
6087  B       b2552   t2552  B       b1431   t1424
6088  T       t2553   o b735 b2552  T       t1431   o b735 b1431
6089  B       b2553   t2553  B       b1567   t1431
6090  T       t2554   o b723 b2553  T       t1567   o b723 b1567
6091  B       b2554   t2554  B       b1568   t1567
6092  T       t2555   o b709 b2554  T       t1568   o b709 b1568
6093  B       b2555   t2555  B       b1636   t1568
6094  T       t2556   o b693 b2555  T       t1636   o b693 b1636
6095  B       b2556   t2556  B       b1643   t1636
6096  T       t2557   o b671 b2556  T       t1643   o b671 b1643
6097  B       b2557   t2557  B       b1644   t1643
6098  T       t2558   o b652 b2557  T       t1644   o b652 b1644
6099  B       b2558   t2558  B       b1645   t1644
6100  T       t2559   o b632 b2558  T       t1645   o b632 b1645
6101  B       b2559   t2559  B       b1648   t1645
6102  T       t2560   o b614 b2559  T       t1648   o b614 b1648
6103  B       b2560   t2560  B       b1649   t1648
6104  T       t2561   o b606 b2560  T       t1649   o b606 b1649
6105  B       b2561   t2561  B       b1650   t1649
6106  T       t2562   o b592 b2561  T       t1650   o b592 b1650
6107  B       b2562   t2562  B       b1651   t1650
6108  T       t2563   o b585 b2562  T       t1651   o b585 b1651
6109  B       b2563   t2563  B       b1652   t1651
6110  T       t2564   o b576 b2563  T       t1652   o b576 b1652
6111  B       b2564   t2564  B       b1653   t1652
6112  T       t2565   o b569 b2564  T       t1653   o b569 b1653
6113  B       b2565   t2565  B       b1654   t1653
6114  T       t2566   o b564 b2565  T       t1654   o b564 b1654
6115  B       b2566   t2566  B       b1655   t1654
6116  T       t2567   o b556 b2566  T       t1655   o b556 b1655
6117  B       b2567   t2567  B       b1658   t1655
6118  T       t2568   o b551 b2567  T       t1658   o b551 b1658
6119  B       b2568   t2568  B       b1659   t1658
6120  T       t2569   o b544 b2568  T       t1659   o b544 b1659
6121  B       b2569   t2569  B       b1684   t1659
6122  T       t2570   o b537 b2569  T       t1684   o b537 b1684
6123  B       b2570   t2570  B       b1685   t1684
6124  T       t2571   o b530 b2570  T       t1685   o b530 b1685
6125  B       b2571   t2571  B       b1686   t1685
6126  T       t2572   o b523 b2571  T       t1686   o b523 b1686
6127  B       b2572   t2572  B       b1689   t1686
6128  T       t2573   o b515 b2572  T       t1689   o b515 b1689
6129  B       b2573   t2573  B       b1690   t1689
6130  T       t2574   o b507 b2573  T       t1690   o b507 b1690
6131  B       b2574   t2574  B       b1691   t1690
6132  T       t2575   o b499 b2574  T       t1691   o b499 b1691
6133  B       b2575   t2575  B       b1692   t1691
6134  T       t2576   o b492 b2575  T       t1692   o b492 b1692
6135  B       b2576   t2576  B       b1693   t1692
6136  T       t2577   o b485 b2576  T       t1693   o b485 b1693
6137  B       b2577   t2577  B       b1694   t1693
6138  T       t2578   o b478 b2577  T       t1694   o b478 b1694
6139  B       b2578   t2578  B       b1695   t1694
6140  T       t2579   o b469 b2578  T       t1695   o b469 b1695
6141  B       b2579   t2579  B       b1696   t1695
6142  T       t2580   o b460 b2579  T       t1696   o b460 b1696
6143  B       b2580   t2580  B       b1699   t1696
6144  T       t2581   o b451 b2580  T       t1699   o b451 b1699
6145  B       b2581   t2581  B       b1700   t1699
6146  T       t2582   o b442 b2581  T       t1700   o b442 b1700
6147  B       b2582   t2582  B       b1724   t1700
6148  T       t2583   o b433 b2582  T       t1724   o b433 b1724
6149  B       b2583   t2583  B       b1725   t1724
6150  T       t2584   o b424 b2583  T       t1725   o b424 b1725
6151  B       b2584   t2584  B       b1736   t1725
6152  T       t2585   o b415 b2584  T       t1750   o b415 b1736
6153  B       b2585   t2585  B       b1837   t1750
6154  T       t2586   o b405 b2585  T       t1837   o b405 b1837
6155  B       b2586   t2586  B       b1844   t1837
6156  T       t2587   o b398 b2586  T       t1844   o b398 b1844
6157  B       b2587   t2587  B       b1846   t1844
6158  T       t2588   o b390 b2587  T       t1904   o b390 b1846
6159  B       b2588   t2588  B       b1905   t1904
6160  T       t2589   o b384 b2588  T       t1905   o b384 b1905
6161  B       b2589   t2589  B       b1912   t1905
6162  T       t2590   o b369 b2589  T       t1912   o b369 b1912
6163  B       b2590   t2590  B       b1913   t1912
6164  T       t2591   o b367 b2590  T       t1913   o b367 b1913
6165  B       b2591   t2591  B       b1952   t1913
6166  T       t2592   o b358 b2591  T       t1960   o b358 b1952

Legend:
Removed from v.3405  
changed lines
  Added in v.3463

  ViewVC Help
Powered by ViewVC 1.1.26