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

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

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

revision 3572 by xiny, Tue Apr 2 08:46:33 2002 UTC revision 3573 by xiny, Tue Apr 9 06:02:02 2002 UTC
# Line 5  Line 5 
5  NSummary        Summary Summary NIL  NSummary        Summary Summary NIL
6  NSummary!location       location        location Summary  NSummary!location       location        location Summary
7  P       p       Number 0  P       p       Number 0
8  P       p1      Number 19  P       p3      Number 21
9  O       o1      location p p1  O       o6      location p p3
10  NSummary!parent parent  parent Summary  NSummary!parent parent  parent Summary
11  O       o2      parent  O       o2      parent
12  P       p2      String Czf_itt_set  P       p2      String Czf_itt_set
# Line 495  Line 495 
495  B       b173    t173  B       b173    t173
496  T       t174    o b83 b173  T       t174    o b83 b173
497  B       b174    t174  B       b174    t174
 T       t175    o b81 b174  
 B       b175    t175  
 T       t176    o b79 b175  
 B       b176    t176  
 T       t177    o b77 b176  
 B       b177    t177  
 T       t178    o b75 b177  
 B       b178    t178  
 T       t179    o b73 b178  
 B       b179    t179  
 T       t180    o b71 b179  
 B       b180    t180  
 T       t181    o b69 b180  
 B       b181    t181  
 T       t182    o b67 b181  
 B       b182    t182  
 T       t183    o b65 b182  
 B       b183    t183  
 T       t184    o b63 b183  
 B       b184    t184  
 T       t185    o b61 b184  
 B       b185    t185  
 T       t186    o b59 b185  
 B       b186    t186  
 T       t187    o b57 b186  
 B       b187    t187  
 T       t188    o b55 b187  
 B       b188    t188  
 T       t189    o b53 b188  
 B       b189    t189  
 T       t190    o b51 b189  
 B       b190    t190  
 T       t191    o b49 b190  
 B       b191    t191  
 T       t192    o b47 b191  
 B       b192    t192  
 T       t193    o b45 b192  
 B       b193    t193  
 T       t194    o b43 b193  
 B       b194    t194  
 T       t195    o b41 b194  
 B       b195    t195  
 T       t196    o b39 b195  
 B       b196    t196  
 T       t197    o b37 b196  
 B       b197    t197  
 T       t198    o b35 b197  
 B       b198    t198  
 T       t199    o b33 b198  
 B       b199    t199  
 T       t200    o b31 b199  
 B       b200    t200  
 T       t201    o b29 b200  
 B       b201    t201  
 T       t202    o b27 b201  
 B       b202    t202  
 T       t203    o b25 b202  
 B       b203    t203  
 T       t204    o b23 b203  
 B       b204    t204  
 T       t205    o b21 b204  
 B       b205    t205  
 T       t206    o b19 b205  
 B       b206    t206  
 T       t207    o b17 b206  
 B       b207    t207  
 T       t208    o b15 b207  
 B       b208    t208  
 T       t209    o b13 b208  
 B       b209    t209  
 T       t210    o b11 b209  
 B       b210    t210  
 T       t211    o b9 b210  
 B       b211    t211  
 T       t212    o b7 b211  
 B       b212    t212  
 T       t213    o b5 b212  
 B       b213    t213  
498  NSummary!resource       resource        resource Summary  NSummary!resource       resource        resource Summary
499  P       p213    String auto  P       p213    String auto
500  O       o213    resource p213  O       o213    resource p213
# Line 960  Line 882 
882  B       b355    t355  B       b355    t355
883  T       t356    o b228 b355  T       t356    o b228 b355
884  B       b356    t356  B       b356    t356
 T       t357    o2 b5 b213 b356  
 B       b357    t357  
 T       t358    o1 b357  
 B       b358    t358  
 P       p358    Number 20  
 P       p359    Number 41  
 O       o359    location p358 p359  
885  P       p360    String Czf_itt_group  P       p360    String Czf_itt_group
886  O       o360    parent p360  O       o360    parent p360
887  T       t360    o360  T       t360    o360
# Line 1027  Line 942 
942  B       b378    t378  B       b378    t378
943  T       t379    o b378 b4  T       t379    o b378 b4
944  B       b379    t379  B       b379    t379
 T       t380    o b379 b4  
 B       b380    t380  
 T       t381    o b377 b380  
 B       b381    t381  
 T       t382    o b375 b381  
 B       b382    t382  
 T       t383    o b373 b382  
 B       b383    t383  
 T       t384    o b371 b383  
 B       b384    t384  
 T       t385    o b369 b384  
 B       b385    t385  
 T       t386    o b367 b385  
 B       b386    t386  
 T       t387    o b365 b386  
 B       b387    t387  
 T       t388    o b363 b387  
 B       b388    t388  
 P       p391    Number 42  
 P       p392    Number 63  
 O       o392    location p391 p392  
945  P       p393    String Czf_itt_equiv  P       p393    String Czf_itt_equiv
946  O       o393    parent p393  O       o393    parent p393
947  T       t393    o393  T       t393    o393
# Line 1084  Line 978 
978  B       b403    t403  B       b403    t403
979  T       t404    o b403 b4  T       t404    o b403 b4
980  B       b404    t404  B       b404    t404
981  T       t1      o b404 b388  T       t257    o b75 b174
982  B       b1      t1  B       b257    t257
983  T       t2      o b402 b1  T       t265    o b81 b257
984  B       b2      t2  B       b265    t265
985  T       t3      o b400 b2  T       t266    o b73 b265
986  B       b3      t3  B       b266    t266
987  T       t214    o b398 b3  T       t289    o b71 b266
988  B       b214    t214  B       b289    t289
989  T       t215    o b396 b214  T       t290    o b69 b289
990  B       b215    t215  B       b290    t290
991  T       t218    o b394 b215  T       t292    o b79 b290
992  B       b218    t218  B       b292    t292
993  T       t219    o b361 b218  T       t300    o b67 b292
994  B       b219    t219  B       b300    t300
995  T       t229    o2 b361 b219 b356  T       t301    o b65 b300
996  B       b229    t229  B       b301    t301
997  T       t230    o359 b229  T       t304    o b63 b301
998  B       b230    t230  B       b304    t304
999    T       t315    o b61 b304
1000    B       b315    t315
1001    T       t327    o b59 b315
1002    B       b327    t327
1003    T       t331    o b77 b327
1004    B       b331    t331
1005    T       t332    o b57 b331
1006    B       b332    t332
1007    T       t359    o b55 b332
1008    B       b359    t359
1009    T       t389    o b53 b359
1010    B       b389    t389
1011    T       t390    o b47 b389
1012    B       b390    t390
1013    T       t391    o b45 b390
1014    B       b391    t391
1015    T       t392    o b379 b391
1016    B       b392    t392
1017    T       t405    o b377 b392
1018    B       b405    t405
1019    T       t413    o b51 b405
1020    B       b413    t413
1021    T       t419    o b49 b413
1022    B       b419    t419
1023    T       t420    o b43 b419
1024    B       b420    t420
1025    T       t421    o b41 b420
1026    B       b421    t421
1027    T       t424    o b39 b421
1028    B       b424    t424
1029    T       t425    o b37 b424
1030    B       b425    t425
1031    T       t426    o b35 b425
1032    B       b426    t426
1033    T       t427    o b33 b426
1034    B       b427    t427
1035    T       t428    o b31 b427
1036    B       b428    t428
1037    T       t431    o b29 b428
1038    B       b431    t431
1039    T       t432    o b27 b431
1040    B       b432    t432
1041    T       t433    o b25 b432
1042    B       b433    t433
1043    T       t434    o b23 b433
1044    B       b434    t434
1045    T       t441    o b21 b434
1046    B       b441    t441
1047    T       t442    o b19 b441
1048    B       b442    t442
1049    T       t443    o b17 b442
1050    B       b443    t443
1051    T       t444    o b15 b443
1052    B       b444    t444
1053    T       t445    o b13 b444
1054    B       b445    t445
1055    T       t450    o b11 b445
1056    B       b450    t450
1057    T       t451    o b9 b450
1058    B       b451    t451
1059    T       t452    o b7 b451
1060    B       b452    t452
1061    T       t453    o b5 b452
1062    B       b453    t453
1063    T       t459    o b375 b453
1064    B       b459    t459
1065    T       t460    o b373 b459
1066    B       b460    t460
1067    T       t461    o b371 b460
1068    B       b461    t461
1069    T       t462    o b369 b461
1070    B       b462    t462
1071    T       t463    o b367 b462
1072    B       b463    t463
1073    T       t468    o b365 b463
1074    B       b468    t468
1075    T       t469    o b363 b468
1076    B       b469    t469
1077    T       t470    o b404 b469
1078    B       b470    t470
1079    T       t471    o b402 b470
1080    B       b471    t471
1081    T       t477    o b400 b471
1082    B       b477    t477
1083    T       t478    o b398 b477
1084    B       b478    t478
1085    T       t479    o b396 b478
1086    B       b479    t479
1087    T       t486    o b394 b479
1088    B       b486    t486
1089    T       t487    o b361 b486
1090    B       b487    t487
1091    T       t488    o2 b361 b487 b356
1092    B       b488    t488
1093    T       t489    o6 b488
1094    B       b489    t489
1095    P       p489    Number 22
1096    P       p492    Number 46
1097    O       o492    location p489 p492
1098  T       t233    o2 b394 b4 b356  T       t233    o2 b394 b4 b356
1099  B       b233    t233  B       b233    t233
 T       t237    o392 b233  
 B       b237    t237  
 P       p412    Number 64  
 P       p413    Number 90  
 O       o413    location p412 p413  
1100  P       p414    String Czf_itt_abel_group  P       p414    String Czf_itt_abel_group
1101  O       o414    parent p414  O       o414    parent p414
1102  T       t414    o414  T       t414    o414
# Line 1119  Line 1107 
1107  B       b416    t416  B       b416    t416
1108  T       t417    o2 b415 b416 b356  T       t417    o2 b415 b416 b356
1109  B       b417    t417  B       b417    t417
1110  T       t418    o413 b417  P       p34     String Czf_itt_set_bvd
1111  B       b418    t418  O       o34     parent p34
1112  P       p418    Number 92  T       t716    o34
1113  P       p419    Number 103  B       b1443   t716
1114  O       o419    location p418 p419  T       t1455   o b1443 b4
1115    B       b2257   t1455
1116    T       t2257   o b2257 b4
1117    B       b2258   t2257
1118    T       t2258   o2 b2257 b2258 b356
1119    B       b2259   t2258
1120    P       p2262   String Czf_itt_subgroup
1121    O       o2262   parent p2262
1122    T       t2262   o2262
1123    B       b2262   t2262
1124    T       t2263   o b2262 b4
1125    B       b2263   t2263
1126    P       p493    String Czf_itt_group_bvd
1127    O       o493    parent p493
1128    T       t495    o493
1129    B       b495    t495
1130    T       t496    o b495 b4
1131    B       b496    t496
1132    P       p2263   String Czf_itt_isect
1133    O       o2263   parent p2263
1134    T       t2264   o2263
1135    B       b2264   t2264
1136    T       t2265   o b2264 b4
1137    B       b2265   t2265
1138    T       t2266   o b2265 b4
1139    B       b2266   t2266
1140    T       t497    o b496 b2266
1141    B       b497    t497
1142    T       t504    o b2263 b497
1143    B       b504    t504
1144    T       t505    o2 b2263 b504 b356
1145    B       b505    t505
1146    T       t506    o492 b505
1147    B       b506    t506
1148    P       p506    Number 47
1149    P       p507    Number 73
1150    O       o507    location p506 p507
1151    T       t511    o507 b417
1152    B       b511    t511
1153    P       p511    Number 74
1154    P       p512    Number 95
1155    O       o512    location p511 p512
1156    T       t512    o512 b233
1157    B       b512    t512
1158    P       p513    Number 96
1159    P       p514    Number 121
1160    O       o514    location p513 p514
1161    T       t522    o2 b496 b4 b356
1162    B       b522    t522
1163    T       t570    o514 b522
1164    B       b570    t570
1165    P       p570    Number 122
1166    P       p571    Number 145
1167    O       o571    location p570 p571
1168    T       t571    o571 b2259
1169    B       b571    t571
1170    P       p572    Number 146
1171    P       p573    Number 171
1172    O       o573    location p572 p573
1173    P       p2271   String Czf_itt_inv_image
1174    O       o2271   parent p2271
1175    T       t2271   o2271
1176    B       b2271   t2271
1177    T       t2272   o b2271 b4
1178    B       b2272   t2272
1179    T       t2273   o b2272 b4
1180    B       b2273   t2273
1181    T       t2274   o2 b2272 b2273 b356
1182    B       b2274   t2274
1183    T       t575    o573 b2274
1184    B       b575    t575
1185    P       p1      Number 172
1186    P       p4      Number 193
1187    O       o8      location p1 p4
1188    P       p12     String Czf_itt_coset
1189    O       o14     parent p12
1190    T       t175    o14
1191    B       b175    t175
1192    T       t176    o b175 b4
1193    B       b176    t176
1194    T       t177    o b176 b4
1195    B       b177    t177
1196    T       t178    o2 b176 b177 b356
1197    B       b178    t178
1198    T       t179    o8 b178
1199    B       b179    t179
1200    P       p24     Number 194
1201    P       p30     Number 225
1202    O       o30     location p24 p30
1203    P       p32     String Czf_itt_normal_subgroup
1204    O       o32     parent p32
1205    T       t774    o32
1206    B       b3283   t774
1207    T       t3297   o b3283 b4
1208    B       b3359   t3297
1209    T       t3370   o b3359 b4
1210    B       b3734   t3370
1211    T       t3748   o2 b3359 b3734 b356
1212    B       b3954   t3748
1213    T       t3984   o30 b3954
1214    B       b4473   t3984
1215    P       p4475   Number 227
1216    P       p4476   Number 238
1217    O       o4476   location p4475 p4476
1218  NSummary!summary_item   summary_item    summary_item Summary  NSummary!summary_item   summary_item    summary_item Summary
1219  O       o420    summary_item  O       o420    summary_item
1220  NOcaml!str_open str_open        str_open Ocaml  NOcaml!str_open str_open        str_open Ocaml
1221  O       o421    str_open p418 p419  O       o4477   str_open p4475 p4476
1222  NOcaml!string   string  string Ocaml  NOcaml!string   string  string Ocaml
1223  P       p421    String Printf  P       p421    String Printf
1224  O       o422    string p421  O       o422    string p421
# Line 1135  Line 1226 
1226  B       b422    t422  B       b422    t422
1227  T       t423    o b422 b4  T       t423    o b422 b4
1228  B       b423    t423  B       b423    t423
1229  T       t424    o421 b423  T       t4482   o4477 b423
1230  B       b424    t424  B       b5938   t4482
1231  T       t425    o420 b424  T       t5938   o420 b5938
1232  B       b425    t425  B       b5939   t5938
1233  T       t426    o419 b425  T       t5939   o4476 b5939
1234  B       b426    t426  B       b5940   t5939
1235  P       p426    Number 104  P       p5940   Number 239
1236  P       p427    Number 117  P       p5941   Number 252
1237  O       o427    location p426 p427  O       o5941   location p5940 p5941
1238  O       o428    str_open p426 p427  O       o5942   str_open p5940 p5941
1239  P       p428    String Mp_debug  P       p428    String Mp_debug
1240  O       o429    string p428  O       o429    string p428
1241  T       t429    o429  T       t429    o429
1242  B       b429    t429  B       b429    t429
1243  T       t430    o b429 b4  T       t430    o b429 b4
1244  B       b430    t430  B       b430    t430
1245  T       t431    o428 b430  T       t5942   o5942 b430
1246  B       b431    t431  B       b5942   t5942
1247  T       t432    o420 b431  T       t5943   o420 b5942
1248  B       b432    t432  B       b5943   t5943
1249  T       t433    o427 b432  T       t5944   o5941 b5943
1250  B       b433    t433  B       b5944   t5944
1251  P       p433    Number 118  P       p5944   Number 253
1252  P       p434    Number 147  P       p5945   Number 282
1253  O       o434    location p433 p434  O       o5945   location p5944 p5945
1254  O       o435    str_open p433 p434  O       o5946   str_open p5944 p5945
1255  P       p435    String Refiner  P       p435    String Refiner
1256  O       o436    string p435  O       o436    string p435
1257  T       t436    o436  T       t436    o436
# Line 1175  Line 1266 
1266  B       b439    t439  B       b439    t439
1267  T       t440    o b436 b439  T       t440    o b436 b439
1268  B       b440    t440  B       b440    t440
1269  T       t441    o435 b440  T       t5946   o5946 b440
1270  B       b441    t441  B       b5946   t5946
1271  T       t442    o420 b441  T       t5947   o420 b5946
1272  B       b442    t442  B       b5947   t5947
1273  T       t443    o434 b442  T       t5948   o5945 b5947
1274  B       b443    t443  B       b5948   t5948
1275  P       p443    Number 148  P       p5948   Number 283
1276  P       p444    Number 173  P       p5949   Number 308
1277  O       o444    location p443 p444  O       o5949   location p5948 p5949
1278  O       o445    str_open p443 p444  O       o5950   str_open p5948 p5949
1279  P       p445    String Term  P       p445    String Term
1280  O       o446    string p445  O       o446    string p445
1281  T       t446    o446  T       t446    o446
# Line 1195  Line 1286 
1286  B       b448    t448  B       b448    t448
1287  T       t449    o b436 b448  T       t449    o b436 b448
1288  B       b449    t449  B       b449    t449
1289  T       t450    o445 b449  T       t5950   o5950 b449
1290  B       b450    t450  B       b5950   t5950
1291  T       t451    o420 b450  T       t5951   o420 b5950
1292  B       b451    t451  B       b5951   t5951
1293  T       t452    o444 b451  T       t5952   o5949 b5951
1294  B       b452    t452  B       b5952   t5952
1295  P       p452    Number 174  P       p5952   Number 309
1296  P       p453    Number 201  P       p5953   Number 336
1297  O       o453    location p452 p453  O       o5953   location p5952 p5953
1298  O       o454    str_open p452 p453  O       o5954   str_open p5952 p5953
1299  P       p454    String TermOp  P       p454    String TermOp
1300  O       o455    string p454  O       o455    string p454
1301  T       t455    o455  T       t455    o455
# Line 1215  Line 1306 
1306  B       b457    t457  B       b457    t457
1307  T       t458    o b436 b457  T       t458    o b436 b457
1308  B       b458    t458  B       b458    t458
1309  T       t459    o454 b458  T       t5954   o5954 b458
1310  B       b459    t459  B       b5954   t5954
1311  T       t460    o420 b459  T       t5955   o420 b5954
1312  B       b460    t460  B       b5955   t5955
1313  T       t461    o453 b460  T       t5956   o5953 b5955
1314  B       b461    t461  B       b5956   t5956
1315  P       p461    Number 202  P       p5956   Number 337
1316  P       p462    Number 231  P       p5957   Number 366
1317  O       o462    location p461 p462  O       o5957   location p5956 p5957
1318  O       o463    str_open p461 p462  O       o5958   str_open p5956 p5957
1319  P       p463    String TermAddr  P       p463    String TermAddr
1320  O       o464    string p463  O       o464    string p463
1321  T       t464    o464  T       t464    o464
# Line 1235  Line 1326 
1326  B       b466    t466  B       b466    t466
1327  T       t467    o b436 b466  T       t467    o b436 b466
1328  B       b467    t467  B       b467    t467
1329  T       t468    o463 b467  T       t5958   o5958 b467
1330  B       b468    t468  B       b5958   t5958
1331  T       t469    o420 b468  T       t5959   o420 b5958
1332  B       b469    t469  B       b5959   t5959
1333  T       t470    o462 b469  T       t5960   o5957 b5959
1334  B       b470    t470  B       b5960   t5960
1335  P       p470    Number 232  P       p5960   Number 367
 P       p471    Number 260  
 O       o471    location p470 p471  
 O       o472    str_open p470 p471  
1336  P       p472    String TermMan  P       p472    String TermMan
1337  O       o473    string p472  O       o473    string p472
1338  T       t473    o473  T       t473    o473
# Line 1255  Line 1343 
1343  B       b475    t475  B       b475    t475
1344  T       t476    o b436 b475  T       t476    o b436 b475
1345  B       b476    t476  B       b476    t476
 T       t477    o472 b476  
 B       b477    t477  
 T       t478    o420 b477  
 B       b478    t478  
 T       t479    o471 b478  
 B       b479    t479  
 P       p479    Number 261  
 P       p480    Number 291  
 O       o480    location p479 p480  
 O       o481    str_open p479 p480  
1346  P       p481    String TermSubst  P       p481    String TermSubst
1347  O       o482    string p481  O       o482    string p481
1348  T       t482    o482  T       t482    o482
# Line 1275  Line 1353 
1353  B       b484    t484  B       b484    t484
1354  T       t485    o b436 b484  T       t485    o b436 b484
1355  B       b485    t485  B       b485    t485
1356  T       t486    o481 b485  P       p211    Number 395
1357  B       b486    t486  O       o5960   location p5960 p211
1358  T       t487    o420 b486  O       o5961   str_open p5960 p211
1359  B       b487    t487  T       t5961   o5961 b476
1360  T       t488    o480 b487  B       b5961   t5961
1361  B       b488    t488  T       t5962   o420 b5961
1362  P       p488    Number 292  B       b5962   t5962
1363  P       p489    Number 319  T       t5963   o5960 b5962
1364  O       o489    location p488 p489  B       b5963   t5963
1365  O       o490    str_open p488 p489  P       p5963   Number 396
1366    P       p5964   Number 426
1367    O       o5964   location p5963 p5964
1368    O       o5965   str_open p5963 p5964
1369    T       t5965   o5965 b485
1370    B       b5965   t5965
1371    T       t5966   o420 b5965
1372    B       b5966   t5966
1373    T       t5967   o5964 b5966
1374    B       b5967   t5967
1375    P       p5967   Number 427
1376    P       p5968   Number 454
1377    O       o5968   location p5967 p5968
1378    O       o5969   str_open p5967 p5968
1379  P       p490    String Refine  P       p490    String Refine
1380  O       o491    string p490  O       o491    string p490
1381  T       t491    o491  T       t491    o491
# Line 1295  Line 1386 
1386  B       b493    t493  B       b493    t493
1387  T       t494    o b436 b493  T       t494    o b436 b493
1388  B       b494    t494  B       b494    t494
1389  T       t495    o490 b494  T       t5969   o5969 b494
1390  B       b495    t495  B       b5969   t5969
1391  T       t496    o420 b495  T       t5970   o420 b5969
1392  B       b496    t496  B       b5970   t5970
1393  T       t497    o489 b496  T       t5971   o5968 b5970
1394  B       b497    t497  B       b5971   t5971
1395  P       p497    Number 320  P       p225    Number 455
1396  P       p498    Number 352  P       p5971   Number 487
1397  O       o498    location p497 p498  O       o5971   location p225 p5971
1398  O       o499    str_open p497 p498  O       o5972   str_open p225 p5971
1399  P       p499    String RefineError  P       p499    String RefineError
1400  O       o500    string p499  O       o500    string p499
1401  T       t500    o500  T       t500    o500
# Line 1315  Line 1406 
1406  B       b502    t502  B       b502    t502
1407  T       t503    o b436 b502  T       t503    o b436 b502
1408  B       b503    t503  B       b503    t503
1409  T       t504    o499 b503  T       t5972   o5972 b503
1410  B       b504    t504  B       b5972   t5972
1411  T       t505    o420 b504  T       t5973   o420 b5972
1412  B       b505    t505  B       b5973   t5973
1413  T       t506    o498 b505  T       t5974   o5971 b5973
1414  B       b506    t506  B       b5974   t5974
1415  P       p506    Number 353  P       p5974   Number 488
1416  P       p507    Number 369  P       p5975   Number 504
1417  O       o507    location p506 p507  O       o5975   location p5974 p5975
1418  O       o508    str_open p506 p507  O       o5976   str_open p5974 p5975
1419  P       p508    String Mp_resource  P       p508    String Mp_resource
1420  O       o509    string p508  O       o509    string p508
1421  T       t509    o509  T       t509    o509
1422  B       b509    t509  B       b509    t509
1423  T       t510    o b509 b4  T       t510    o b509 b4
1424  B       b510    t510  B       b510    t510
1425  T       t511    o508 b510  T       t5976   o5976 b510
1426  B       b511    t511  B       b5976   t5976
1427  T       t512    o420 b511  T       t5977   o420 b5976
1428  B       b512    t512  B       b5977   t5977
1429  T       t513    o507 b512  T       t5978   o5975 b5977
1430  B       b513    t513  B       b5978   t5978
1431  P       p246    Number 370  P       p5978   Number 505
1432  P       p514    Number 387  P       p5979   Number 522
1433  O       o246    location p246 p514  O       o5979   location p5978 p5979
1434  O       o247    str_open p246 p514  O       o5980   str_open p5978 p5979
1435  P       p247    String Simple_print  P       p247    String Simple_print
1436  O       o248    string p247  O       o248    string p247
1437  T       t251    o248  T       t251    o248
1438  B       b251    t251  B       b251    t251
1439  T       t256    o b251 b4  T       t256    o b251 b4
1440  B       b256    t256  B       b256    t256
1441  T       t257    o247 b256  T       t5980   o5980 b256
1442  B       b257    t257  B       b5980   t5980
1443  T       t265    o420 b257  T       t5981   o420 b5980
1444  B       b265    t265  B       b5981   t5981
1445  T       t266    o246 b265  T       t5982   o5979 b5981
1446  B       b266    t266  B       b5982   t5982
1447  P       p277    Number 389  P       p5982   Number 524
1448  P       p279    Number 405  P       p5983   Number 540
1449  O       o279    location p277 p279  O       o5983   location p5982 p5983
1450  O       o280    str_open p277 p279  O       o5984   str_open p5982 p5983
1451  P       p515    String Tactic_type  P       p515    String Tactic_type
1452  O       o516    string p515  O       o516    string p515
1453  T       t516    o516  T       t516    o516
1454  B       b516    t516  B       b516    t516
1455  T       t517    o b516 b4  T       t517    o b516 b4
1456  B       b517    t517  B       b517    t517
1457  T       t289    o280 b517  T       t5984   o5984 b517
1458  B       b289    t289  B       b5984   t5984
1459  T       t290    o420 b289  T       t5985   o420 b5984
1460  B       b290    t290  B       b5985   t5985
1461  T       t292    o279 b290  T       t5986   o5983 b5985
1462  B       b292    t292  B       b5986   t5986
1463  P       p294    Number 406  P       p5986   Number 541
1464  P       p295    Number 432  P       p5987   Number 567
1465  O       o295    location p294 p295  O       o5987   location p5986 p5987
1466  O       o296    str_open p294 p295  O       o5988   str_open p5986 p5987
1467  P       p522    String Tacticals  P       p522    String Tacticals
1468  O       o523    string p522  O       o523    string p522
1469  T       t523    o523  T       t523    o523
# Line 1381  Line 1472 
1472  B       b524    t524  B       b524    t524
1473  T       t525    o b516 b524  T       t525    o b516 b524
1474  B       b525    t525  B       b525    t525
1475  T       t300    o296 b525  T       t5988   o5988 b525
1476  B       b300    t300  B       b5988   t5988
1477  T       t301    o420 b300  T       t5989   o420 b5988
1478  B       b301    t301  B       b5989   t5989
1479  T       t304    o295 b301  T       t5990   o5987 b5989
1480  B       b304    t304  B       b5990   t5990
1481  P       p307    Number 433  P       p5990   Number 568
 P       p322    Number 457  
 O       o322    location p307 p322  
 O       o323    str_open p307 p322  
1482  P       p530    String Sequent  P       p530    String Sequent
1483  O       o531    string p530  O       o531    string p530
1484  T       t531    o531  T       t531    o531
# Line 1399  Line 1487 
1487  B       b532    t532  B       b532    t532
1488  T       t533    o b516 b532  T       t533    o b516 b532
1489  B       b533    t533  B       b533    t533
 T       t327    o323 b533  
 B       b327    t327  
 T       t331    o420 b327  
 B       b331    t331  
 T       t332    o322 b331  
 B       b332    t332  
 P       p337    Number 458  
 P       p344    Number 488  
 O       o344    location p337 p344  
 O       o345    str_open p337 p344  
1490  P       p538    String Conversionals  P       p538    String Conversionals
1491  O       o539    string p538  O       o539    string p538
1492  T       t539    o539  T       t539    o539
# Line 1417  Line 1495 
1495  B       b540    t540  B       b540    t540
1496  T       t541    o b516 b540  T       t541    o b516 b540
1497  B       b541    t541  B       b541    t541
 T       t359    o345 b541  
 B       b359    t359  
 T       t392    o420 b359  
 B       b392    t392  
 T       t413    o344 b392  
 B       b413    t413  
 P       p415    Number 489  
 P       p416    Number 499  
 O       o416    location p415 p416  
 O       o417    str_open p415 p416  
1498  O       o547    string p131  O       o547    string p131
1499  T       t547    o547  T       t547    o547
1500  B       b547    t547  B       b547    t547
1501  T       t548    o b547 b4  T       t548    o b547 b4
1502  B       b548    t548  B       b548    t548
 T       t419    o417 b548  
 B       b419    t419  
 T       t420    o420 b419  
 B       b420    t420  
 T       t421    o416 b420  
 B       b421    t421  
 P       p422    Number 500  
 P       p423    Number 508  
 O       o423    location p422 p423  
 O       o424    str_open p422 p423  
1503  O       o554    string p129  O       o554    string p129
1504  T       t554    o554  T       t554    o554
1505  B       b554    t554  B       b554    t554
1506  T       t555    o b554 b4  T       t555    o b554 b4
1507  B       b555    t555  B       b555    t555
1508  T       t427    o424 b555  P       p2269   Number 592
1509  B       b427    t427  O       o5990   location p5990 p2269
1510  T       t428    o420 b427  O       o5991   str_open p5990 p2269
1511  B       b428    t428  T       t5991   o5991 b533
1512  T       t434    o423 b428  B       b5991   t5991
1513  B       b434    t434  T       t5992   o420 b5991
1514    B       b5992   t5992
1515    T       t5993   o5990 b5992
1516    B       b5993   t5993
1517    P       p5993   Number 593
1518    P       p5994   Number 623
1519    O       o5994   location p5993 p5994
1520    O       o5995   str_open p5993 p5994
1521    T       t6004   o5995 b541
1522    B       b6408   t6004
1523    T       t6408   o420 b6408
1524    B       b6409   t6408
1525    T       t6409   o5994 b6409
1526    B       b6410   t6409
1527    P       p6410   Number 624
1528    P       p6411   Number 634
1529    O       o6411   location p6410 p6411
1530    O       o6412   str_open p6410 p6411
1531    T       t6412   o6412 b548
1532    B       b6412   t6412
1533    T       t6413   o420 b6412
1534    B       b6413   t6413
1535    T       t6414   o6411 b6413
1536    B       b6414   t6414
1537    P       p6414   Number 635
1538    P       p6415   Number 643
1539    O       o6415   location p6414 p6415
1540    O       o6416   str_open p6414 p6415
1541    T       t6416   o6416 b555
1542    B       b6416   t6416
1543    T       t6417   o420 b6416
1544    B       b6417   t6417
1545    T       t6418   o6415 b6417
1546    B       b6418   t6418
1547    P       p6418   Number 645
1548    P       p6419   Number 662
1549    O       o6419   location p6418 p6419
1550    O       o6420   str_open p6418 p6419
1551  O       o561    string p119  O       o561    string p119
1552  T       t561    o561  T       t561    o561
1553  B       b561    t561  B       b561    t561
1554  T       t562    o b561 b4  T       t562    o b561 b4
1555  B       b562    t562  B       b562    t562
1556  P       p565    Number 510  T       t6420   o6420 b562
1557  P       p437    Number 527  B       b6420   t6420
1558  O       o438    location p565 p437  T       t6421   o420 b6420
1559  O       o439    str_open p565 p437  B       b6421   t6421
1560  T       t444    o439 b562  T       t6422   o6419 b6421
1561  B       b444    t444  B       b6422   t6422
1562  T       t445    o420 b444  P       p6422   Number 663
1563  B       b445    t445  P       p6423   Number 684
1564  T       t453    o438 b445  O       o6423   location p6422 p6423
1565  B       b453    t453  O       o6424   str_open p6422 p6423
 P       p455    Number 528  
 P       p456    Number 549  
 O       o456    location p455 p456  
 O       o457    str_open p455 p456  
1566  O       o568    string p121  O       o568    string p121
1567  T       t568    o568  T       t568    o568
1568  B       b568    t568  B       b568    t568
1569  T       t569    o b568 b4  T       t569    o b568 b4
1570  B       b569    t569  B       b569    t569
1571  T       t462    o457 b569  T       t6424   o6424 b569
1572  B       b462    t462  B       b6424   t6424
1573  T       t463    o420 b462  T       t6425   o420 b6424
1574  B       b463    t463  B       b6425   t6425
1575  T       t471    o456 b463  T       t6426   o6423 b6425
1576  B       b471    t471  B       b6426   t6426
1577  P       p473    Number 551  P       p2292   Number 686
1578  P       p474    Number 583  P       p6426   Number 718
1579  O       o474    location p473 p474  O       o6426   location p2292 p6426
1580  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1581  P       p574    String hom  P       p574    String hom
1582  O       o574    opname p574  O       o574    opname p574
# Line 1521  Line 1612 
1612  B       b480    t480  B       b480    t480
1613  T       t481    o574 b480  T       t481    o574 b480
1614  B       b481    t481  B       b481    t481
1615  T       t489    o474 b481  T       t6427   o6426 b481
1616  B       b489    t489  B       b6427   t6427
1617  P       p491    Number 585  P       p6427   Number 719
1618  P       p492    Number 709  P       p6428   Number 758
1619  O       o492    location p491 p492  O       o6428   location p6427 p6428
1620    P       p2990   String kernel
1621    O       o2990   opname p2990
1622    NCzf_itt_hom!kernel     kernel  kernel Czf_itt_hom
1623    O       o2992   kernel
1624    P       p2992   Var h
1625    O       o2993   var p2992
1626    T       t2993   o2993
1627    B       b2993   t2993
1628    T       t2997   o2992 b2993 b576 b577 b582
1629    B       b2997   t2997
1630    T       t2998   o2990 b2997
1631    B       b2998   t2998
1632    T       t6428   o6428 b2998
1633    B       b6428   t6428
1634    P       p6429   Number 760
1635    P       p6430   Number 884
1636    O       o6430   location p6429 p6430
1637  T       t583    o575 b576 b577 b578 b579 b582  T       t583    o575 b576 b577 b578 b579 b582
1638  B       b583    t583  B       b583    t583
1639  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
# Line 1590  Line 1698 
1698  B       b515    t515  B       b515    t515
1699  T       t521    o587 b591 b498 b515  T       t521    o587 b591 b498 b515
1700  B       b521    t521  B       b521    t521
1701  T       t522    o492 b521  T       t6430   o6430 b521
1702  B       b522    t522  B       b6430   t6430
1703  P       p523    Number 820  P       p6431   Number 886
1704  P       p3      Number 1255  P       p6432   Number 1038
1705  O       o6      location p523 p3  O       o6432   location p6431 p6432
1706    P       p3005   String kernel_df
1707    O       o3005   dform p3005
1708    T       t3005   o2992 b2993 b576 b577 b592
1709    B       b3005   t3005
1710    P       p3006   String kernel(
1711    O       o3007   string593 p3006
1712    T       t3007   o3007
1713    B       b3007   t3007
1714    T       t3008   o595 b2993
1715    B       b3008   t3008
1716    T       t3009   o b596 b508
1717    B       b3009   t3009
1718    T       t3010   o b3008 b3009
1719    B       b3010   t3010
1720    T       t3011   o b3007 b3010
1721    B       b3011   t3011
1722    T       t3013   o593 b3011
1723    B       b3013   t3013
1724    T       t3014   o3005 b591 b3005 b3013
1725    B       b3014   t3014
1726    T       t6432   o6432 b3014
1727    B       b6432   t6432
1728    P       p6433   Number 1149
1729    P       p6434   Number 1584
1730    O       o6434   location p6433 p6434
1731  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1732  P       p618    String unfold_hom  P       p618    String unfold_hom
1733  O       o618    rewrite p618  O       o618    rewrite p618
# Line 2509  Line 2642 
2642  B       b309    t309  B       b309    t309
2643  T       t310    o618 b480 b309 b655 b4  T       t310    o618 b480 b309 b655 b4
2644  B       b310    t310  B       b310    t310
2645  T       t315    o6 b310  T       t6434   o6434 b310
2646  B       b315    t315  B       b6434   t6434
2647  P       p323    Number 1257  P       p6435   Number 1746
2648  P       p324    Number 1508  P       p3019   String unfold_kernel
2649  O       o324    location p323 p324  O       o3019   rewrite p3019
2650    NCzf_itt_group_bvd      Czf_itt_group_bvd       Czf_itt_group_bvd NIL
2651    NCzf_itt_group_bvd!group_bvd    group_bvd       group_bvd Czf_itt_group_bvd
2652    O       o3020   group_bvd
2653  T       t316    o681 b270  T       t316    o681 b270
2654  S       s316    t664 h  S       s316    t664 h
2655  G       s316    t316  G       s316    t316
# Line 2604  Line 2740 
2740  B       b946    t945  B       b946    t945
2741  T       t946    o690 b946  T       t946    o690 b946
2742  B       b947    t946  B       b947    t946
 P       p325    Number 1281  
 P       p329    Number 1289  
 O       o329    resource_defs p325 p329 p264  
 P       p345    Number 1287  
 O       o346    uid p345 p329  
 T       t389    o346 b784  
 B       b389    t389  
 T       t390    o b389 b4  
 B       b390    t390  
 T       t391    o329 b390  
 B       b391    t391  
 T       t405    o b391 b4  
 B       b405    t405  
 T       t947    o659 b661 b619 b947 b405  
 B       b948    t947  
 T       t948    o324 b948  
 B       b949    t948  
 P       p407    Number 1510  
 P       p408    Number 2208  
 O       o408    location p407 p408  
2743  H       h408    c t634  H       h408    c t634
2744  H       h409    d t634  H       h409    d t634
2745  P       p409    Var c  P       p409    Var c
# Line 2718  Line 2834 
2834  B       b964    t964  B       b964    t964
2835  T       t965    o690 b964  T       t965    o690 b964
2836  B       b965    t965  B       b965    t965
 P       p563    Number 1535  
 P       p564    Number 1543  
 O       o564    resource_defs p563 p564 p264  
 P       p566    Number 1541  
 O       o566    uid p566 p564  
 T       t570    o566 b784  
 B       b570    t570  
 T       t571    o b570 b4  
 B       b571    t571  
 T       t572    o564 b571  
 B       b572    t572  
 T       t575    o b572 b4  
 B       b575    t575  
 T       t966    o792 b661 b563 b965 b575  
 B       b966    t966  
 T       t967    o408 b966  
 B       b967    t967  
 P       p4      Number 2210  
 P       p6      Number 2662  
 O       o8      location p4 p6  
2837  P       p8      String hom_fun  P       p8      String hom_fun
2838  O       o10     rule p8  O       o10     rule p8
2839  H       h586    z1 t634  H       h586    z1 t634
# Line 3996  Line 4092 
4092  B       b5032   t5031  B       b5032   t5031
4093  T       t5032   o690 b5032  T       t5032   o690 b5032
4094  B       b5033   t5032  B       b5033   t5032
 P       p5033   Number 2233  
 P       p5034   Number 2241  
 O       o5034   resource_defs p5033 p5034 p264  
 P       p5035   Number 2239  
 O       o5035   uid p5035 p5034  
 T       t5035   o5035 b784  
 B       b5035   t5035  
 T       t5036   o b5035 b4  
 B       b5036   t5036  
 T       t5037   o5034 b5036  
 B       b5037   t5037  
 T       t5038   o b5037 b4  
 B       b5038   t5038  
 T       t5039   o10 b661 b983 b5033 b5038  
 B       b5039   t5039  
 T       t5040   o8 b5039  
 B       b5040   t5040  
 P       p5040   Number 2664  
 P       p5041   Number 3348  
 O       o5041   location p5040 p5041  
4095  P       p5042   String hom_equiv_fun  P       p5042   String hom_equiv_fun
4096  O       o5042   rule p5042  O       o5042   rule p5042
4097  B       b3917   t676  B       b3917   t676
# Line 4684  Line 4760 
4760  B       b5049   t5049  B       b5049   t5049
4761  T       t5050   o690 b5049  T       t5050   o690 b5049
4762  B       b5050   t5050  B       b5050   t5050
 P       p5050   Number 2693  
 P       p5051   Number 2701  
 O       o5051   resource_defs p5050 p5051 p264  
 P       p5052   Number 2699  
 O       o5052   uid p5052 p5051  
 T       t5052   o5052 b784  
 B       b5052   t5052  
 T       t5053   o b5052 b4  
 B       b5053   t5053  
 T       t5054   o5051 b5053  
 B       b5054   t5054  
 T       t5055   o b5054 b4  
 B       b5055   t5055  
 T       t5056   o5042 b661 b2813 b5050 b5055  
 B       b5056   t5056  
 T       t5057   o5041 b5056  
 B       b5057   t5057  
 P       p14     Number 3580  
 P       p16     Number 3946  
 O       o16     location p14 p16  
4763  P       p18     String trivial_hom  P       p18     String trivial_hom
4764  O       o18     rule p18  O       o18     rule p18
4765  T       t611    o623 b626 b537 b679 b1560  T       t611    o623 b626 b537 b679 b1560
# Line 5078  Line 5134 
5134  B       b1236   t1236  B       b1236   t1236
5135  T       t1237   o18 b661 b1005 b1236 b4  T       t1237   o18 b661 b1005 b1236 b4
5136  B       b1237   t1237  B       b1237   t1237
 T       t1238   o16 b1237  
 B       b1238   t1238  
 P       p12     Number 4056  
 P       p20     Number 4472  
 O       o20     location p12 p20  
5137  P       p2618   String hom_id  P       p2618   String hom_id
5138  O       o2618   rule p2618  O       o2618   rule p2618
5139  T       t2618   o1560 b576  T       t2618   o1560 b576
# Line 6264  Line 6315 
6315  B       b1766   t1765  B       b1766   t1765
6316  T       t1766   o12 b3192 b900 b1766 b4  T       t1766   o12 b3192 b900 b1766 b4
6317  B       b1767   t1766  B       b1767   t1766
 T       t580    o20 b1767  
 B       b611    t580  
 P       p1768   Number 4624  
 P       p611    Number 4914  
 O       o611    location p1768 p611  
6318  P       p1769   String "assumT 3 thenT rwh unfold_hom 2 thenT autoT"  P       p1769   String "assumT 3 thenT rwh unfold_hom 2 thenT autoT"
6319  O       o1769   ext_rule p1769  O       o1769   ext_rule p1769
6320  H       h1769   y_2 t530  H       h1769   y_2 t530
# Line 6883  Line 6929 
6929  B       b2047   t2046  B       b2047   t2046
6930  T       t2047   o690 b2047  T       t2047   o690 b2047
6931  B       b2048   t2047  B       b2048   t2047
 P       p612    Number 4646  
 P       p613    Number 4654  
 O       o613    resource_defs p612 p613 p264  
 P       p614    Number 4652  
 O       o614    uid p614 p613  
 T       t614    o614 b784  
 B       b614    t614  
 T       t682    o b614 b4  
 B       b937    t682  
 T       t937    o613 b937  
 B       b938    t937  
 T       t938    o b938 b4  
 B       b939    t938  
 T       t939    o2618 b3192 b4094 b2048 b939  
 B       b1057   t939  
 T       t1088   o611 b1057  
 B       b1157   t1088  
 P       p22     Number 4916  
 P       p24     Number 5333  
 O       o24     location p22 p24  
6932  P       p26     String hom_id_elim  P       p26     String hom_id_elim
6933  O       o26     rule p26  O       o26     rule p26
6934  P       p28     String J  P       p28     String J
# Line 7441  Line 7467 
7467  B       b2479   t2479  B       b2479   t2479
7468  T       t2480   o26 b1058 b2057 b2479 b4  T       t2480   o26 b1058 b2057 b2479 b4
7469  B       b2480   t2480  B       b2480   t2480
 T       t2481   o24 b2480  
 B       b2481   t2481  
 P       p2481   Number 5335  
 P       p2482   Number 5416  
 O       o2482   location p2481 p2482  
7470  NOcaml!str_let  str_let str_let Ocaml  NOcaml!str_let  str_let str_let Ocaml
 O       o2483   str_let p2481 p2482  
7471  NOcaml!patt_var patt_var        patt_var Ocaml  NOcaml!patt_var patt_var        patt_var Ocaml
 P       p2483   Number 5339  
 O       o2484   patt_var p2483 p2482  
7472  NOcaml!patt_done        patt_done       patt_done Ocaml  NOcaml!patt_done        patt_done       patt_done Ocaml
 O       o2485   patt_done p2481 p2482  
 T       t2485   o2485  
 B       b2485   t2485 homIdT  
 T       t2486   o2484 b2485  
 B       b2486   t2486  
7473  NOcaml!fun      fun     fun Ocaml  NOcaml!fun      fun     fun Ocaml
 O       o2486   fun p2483 p2482  
7474  NOcaml!patt_if  patt_if patt_if Ocaml  NOcaml!patt_if  patt_if patt_if Ocaml
 O       o2487   patt_if p2483 p2482  
 P       p2487   Number 5346  
 P       p2488   Number 5347  
 O       o2488   patt_var p2487 p2488  
7475  NOcaml!patt_body        patt_body       patt_body Ocaml  NOcaml!patt_body        patt_body       patt_body Ocaml
 O       o2489   patt_body p2483 p2482  
 P       p2489   Number 5348  
 P       p2490   Number 5349  
 O       o2490   patt_var p2489 p2490  
7476  NOcaml!let      let     let Ocaml  NOcaml!let      let     let Ocaml
 P       p2491   Number 5355  
 O       o2491   let p2491 p2482  
7477  NOcaml!patt_tuple       patt_tuple      patt_tuple Ocaml  NOcaml!patt_tuple       patt_tuple      patt_tuple Ocaml
 P       p2492   Number 5359  
 P       p2493   Number 5363  
 O       o2493   patt_tuple p2492 p2493  
 P       p2494   Number 5360  
 O       o2494   patt_var p2492 p2494  
7478  NOcaml!patt_tuple_arg   patt_tuple_arg  patt_tuple_arg Ocaml  NOcaml!patt_tuple_arg   patt_tuple_arg  patt_tuple_arg Ocaml
 O       o2495   patt_tuple_arg p2492 p2493  
 P       p2495   Number 5362  
 O       o2496   patt_var p2495 p2493  
7479  NOcaml!patt_tuple_end   patt_tuple_end  patt_tuple_end Ocaml  NOcaml!patt_tuple_end   patt_tuple_end  patt_tuple_end Ocaml
 O       o2497   patt_tuple_end p2492 p2493  
7480  NOcaml!patt_in  patt_in patt_in Ocaml  NOcaml!patt_in  patt_in patt_in Ocaml
 O       o2498   patt_in p2491 p2482  
7481  NOcaml!apply    apply   apply Ocaml  NOcaml!apply    apply   apply Ocaml
 P       p2498   Number 5399  
 O       o2499   apply p2498 p2482  
 P       p2499   Number 5414  
 O       o2500   apply p2498 p2499  
 P       p2500   Number 5412  
 O       o2501   apply p2498 p2500  
7482  NOcaml!lid      lid     lid Ocaml  NOcaml!lid      lid     lid Ocaml
 P       p2501   Number 5410  
 O       o2502   lid p2498 p2501  
7483  O       o2503   lid p26  O       o2503   lid p26
7484  T       t2503   o2503  T       t2503   o2503
7485  B       b2503   t2503  B       b2503   t2503
 T       t2504   o2502 b2503  
 B       b2504   t2504  
 P       p2504   Number 5411  
 O       o2504   lid p2504 p2500  
7486  P       p2505   Var j  P       p2505   Var j
7487  O       o2505   var p2505  O       o2505   var p2505
7488  T       t2505   o2505  T       t2505   o2505
7489  B       b2505   t2505  B       b2505   t2505
 T       t2506   o2504 b2505  
 B       b2506   t2506  
 T       t2507   o2501 b2504 b2506  
 B       b2507   t2507  
 P       p2507   Number 5413  
 O       o2507   lid p2507 p2499  
7490  P       p2508   Var k  P       p2508   Var k
7491  O       o2508   var p2508  O       o2508   var p2508
7492  T       t2508   o2508  T       t2508   o2508
7493  B       b2508   t2508  B       b2508   t2508
 T       t2509   o2507 b2508  
 B       b2509   t2509  
 T       t2510   o2500 b2507 b2509  
 B       b2510   t2510  
 P       p2510   Number 5415  
 O       o2510   lid p2510 p2482  
7494  P       p2511   Var p  P       p2511   Var p
7495  O       o2511   var p2511  O       o2511   var p2511
7496  T       t2511   o2511  T       t2511   o2511
7497  B       b2511   t2511  B       b2511   t2511
 T       t2512   o2510 b2511  
 B       b2512   t2512  
 T       t2513   o2499 b2510 b2512  
 B       b2513   t2513  
 T       t2514   o2498 b2513  
 B       b2514   t2514  
 T       t2515   o2497 b2514  
 B       b2515   t2515 k  
 T       t2516   o2496 b2515  
 B       b2516   t2516  
 T       t2517   o2495 b2516  
 B       b2517   t2517 j  
 T       t2518   o2494 b2517  
 B       b2518   t2518  
 T       t2519   o2493 b2518  
 B       b2519   t2519  
 P       p2519   Number 5366  
 P       p2520   Number 5389  
 O       o2520   apply p2519 p2520  
 P       p2521   Number 5387  
 O       o2521   apply p2519 p2521  
7498  NOcaml!proj     proj    proj Ocaml  NOcaml!proj     proj    proj Ocaml
 P       p2522   Number 5385  
 O       o2522   proj p2519 p2522  
 O       o2523   uid p2519 p2522  
7499  O       o2524   uid p530  O       o2524   uid p530
7500  T       t2524   o2524  T       t2524   o2524
7501  B       b2524   t2524  B       b2524   t2524
 T       t2525   o2523 b2524  
 B       b2525   t2525  
 P       p2525   Number 5374  
 O       o2525   lid p2525 p2522  
7502  P       p2526   String hyp_indices  P       p2526   String hyp_indices
7503  O       o2526   lid p2526  O       o2526   lid p2526
7504  T       t2526   o2526  T       t2526   o2526
7505  B       b2526   t2526  B       b2526   t2526
 T       t2527   o2525 b2526  
 B       b2527   t2527  
 T       t2528   o2522 b2525 b2527  
 B       b2528   t2528  
 P       p2528   Number 5386  
 O       o2528   lid p2528 p2521  
 T       t2529   o2528 b2511  
 B       b2529   t2529  
 T       t2530   o2521 b2528 b2529  
 B       b2530   t2530  
 P       p2530   Number 5388  
 O       o2530   lid p2530 p2520  
7506  P       p2531   Var i  P       p2531   Var i
7507  O       o2531   var p2531  O       o2531   var p2531
7508  T       t2531   o2531  T       t2531   o2531
7509  B       b2531   t2531  B       b2531   t2531
 T       t2532   o2530 b2531  
 B       b2532   t2532  
 T       t2533   o2520 b2530 b2532  
 B       b2533   t2533  
 T       t2534   o b2533 b4  
 B       b2534   t2534  
 T       t2535   o2491 b2519 b2534  
 B       b2535   t2535  
 T       t2536   o2489 b2535  
 B       b2536   t2536 p  
 T       t2537   o2490 b2536  
 B       b2537   t2537  
 T       t2538   o2487 b2537  
 B       b2538   t2538  
 T       t2539   o2486 b2538  
 B       b2539   t2539  
 T       t2540   o2489 b2539  
 B       b2540   t2540 i  
 T       t2541   o2488 b2540  
 B       b2541   t2541  
 T       t2542   o2487 b2541  
 B       b2542   t2542  
 T       t2543   o2486 b2542  
 B       b2543   t2543  
 T       t2544   o2483 b2486 b2543  
 B       b2544   t2544  
 T       t2545   o b2544 b4  
 B       b2545   t2545  
 T       t2546   o2483 b2545  
 B       b2546   t2546  
 T       t2547   o420 b2546  
 B       b2547   t2547  
 T       t2548   o2482 b2547  
 B       b2548   t2548  
 P       p2548   Number 5523  
 P       p2549   Number 5925  
 O       o2549   location p2548 p2549  
7510  P       p1159   String "assumT 3 ttca thenT rwh unfold_hom 2 thenT autoT"  P       p1159   String "assumT 3 ttca thenT rwh unfold_hom 2 thenT autoT"
7511  O       o1159   ext_rule p1159  O       o1159   ext_rule p1159
7512  T       t1178   o b2644 b4  T       t1178   o b2644 b4
# Line 8129  Line 8020 
8020  B       b2254   t2253  B       b2254   t2253
8021  T       t2254   o690 b2254  T       t2254   o690 b2254
8022  B       b2255   t2254  B       b2255   t2254
 P       p2550   Number 5546  
 P       p2551   Number 5554  
 O       o2551   resource_defs p2550 p2551 p264  
 P       p2552   Number 5552  
 O       o2552   uid p2552 p2551  
 T       t2552   o2552 b784  
 B       b2552   t2552  
 T       t2553   o b2552 b4  
 B       b2553   t2553  
 T       t2554   o2551 b2553  
 B       b2554   t2554  
 T       t2555   o b2554 b4  
 B       b2555   t2555  
 T       t2556   o2639 b4098 b4105 b2255 b2555  
 B       b2556   t2556  
 T       t2557   o2549 b2556  
 B       b2557   t2557  
 P       p2557   Number 5927  
 P       p2558   Number 6587  
 O       o2558   location p2557 p2558  
8023  P       p2559   String hom_inv_elim  P       p2559   String hom_inv_elim
8024  O       o2559   rule p2559  O       o2559   rule p2559
8025  T       t2559   o b2639 b4  T       t2559   o b2639 b4
# Line 8643  Line 8514 
8514  B       b2979   t2978  B       b2979   t2978
8515  T       t2979   o2559 b2561 b2573 b2979 b4  T       t2979   o2559 b2561 b2573 b2979 b4
8516  B       b2980   t2979  B       b2980   t2979
 T       t2980   o2558 b2980  
 B       b2981   t2980  
 P       p2981   Number 6589  
 P       p2982   Number 6676  
 O       o2982   location p2981 p2982  
 O       o2983   str_let p2981 p2982  
 P       p2983   Number 6593  
 O       o2984   patt_var p2983 p2982  
 O       o2985   patt_done p2981 p2982  
 T       t2985   o2985  
 B       b2985   t2985 homInvT  
 T       t2986   o2984 b2985  
 B       b2986   t2986  
 O       o2986   fun p2983 p2982  
 O       o2987   patt_if p2983 p2982  
 P       p2987   Number 6601  
 P       p2988   Number 6602  
 O       o2988   patt_var p2987 p2988  
 O       o2989   patt_body p2983 p2982  
 P       p2989   Number 6603  
 P       p2990   Number 6604  
 O       o2990   patt_var p2989 p2990  
 P       p2991   Number 6605  
 P       p2992   Number 6606  
 O       o2992   patt_var p2991 p2992  
 P       p2993   Number 6612  
 O       o2993   let p2993 p2982  
 P       p2994   Number 6616  
 P       p2995   Number 6620  
 O       o2995   patt_tuple p2994 p2995  
 P       p2996   Number 6617  
 O       o2996   patt_var p2994 p2996  
 O       o2997   patt_tuple_arg p2994 p2995  
 P       p2997   Number 6619  
 O       o2998   patt_var p2997 p2995  
 O       o2999   patt_tuple_end p2994 p2995  
 O       o3000   patt_in p2993 p2982  
 P       p3000   Number 6656  
 O       o3001   apply p3000 p2982  
 P       p3001   Number 6674  
 O       o3002   apply p3000 p3001  
 P       p3002   Number 6672  
 O       o3003   apply p3000 p3002  
 P       p3003   Number 6670  
 O       o3004   apply p3000 p3003  
 P       p3004   Number 6668  
 O       o3005   lid p3000 p3004  
8517  O       o3006   lid p2559  O       o3006   lid p2559
8518  T       t3006   o3006  T       t3006   o3006
8519  B       b3006   t3006  B       b3006   t3006
 T       t3007   o3005 b3006  
 B       b3007   t3007  
 P       p3007   Number 6669  
 O       o3007   lid p3007 p3003  
 T       t3008   o3007 b2505  
 B       b3008   t3008  
 T       t3009   o3004 b3007 b3008  
 B       b3009   t3009  
 P       p3009   Number 6671  
 O       o3009   lid p3009 p3002  
 T       t3010   o3009 b2508  
 B       b3010   t3010  
 T       t3011   o3003 b3009 b3010  
 B       b3011   t3011  
 P       p3011   Number 6673  
 O       o3011   lid p3011 p3001  
8520  P       p3012   Var t  P       p3012   Var t
8521  O       o3012   var p3012  O       o3012   var p3012
8522  T       t3012   o3012  T       t3012   o3012
8523  B       b3012   t3012  B       b3012   t3012
8524  T       t3013   o3011 b3012  P       p3323   String hom_subgroup1
8525  B       b3013   t3013  O       o3323   rule p3323
8526  T       t3014   o3002 b3011 b3013  P       p3324   Var h1
8527  B       b3014   t3014  O       o3324   var p3324
8528  P       p3014   Number 6675  T       t3324   o3324
8529  O       o3014   lid p3014 p2982  B       b3324   t3324
8530  T       t3015   o3014 b2511  T       t3325   o1834 b3324
8531  B       b3015   t3015  B       b3325   t3325
8532  T       t3016   o3001 b3014 b3015  P       p3325   Var h2
8533  B       b3016   t3016  O       o3325   var p3325
8534  T       t3017   o3000 b3016  T       t3326   o3325
8535  B       b3017   t3017  B       b3326   t3326
8536  T       t3018   o2999 b3017  T       t3327   o1834 b3326
8537  B       b3018   t3018 k  B       b3327   t3327
8538  T       t3019   o2998 b3018  T       t3328   o b3327 b4
8539  B       b3019   t3019  B       b3328   t3328
8540  T       t3020   o2997 b3019  T       t3329   o b3325 b3328
8541  B       b3020   t3020 j  B       b3329   t3329
8542  T       t3021   o2996 b3020  T       t3330   o b3190 b3329
8543  B       b3021   t3021  B       b3330   t3330
8544  T       t3022   o2995 b3021  T       t3331   o b660 b3330
8545  B       b3022   t3022  B       b3331   t3331
8546  P       p3022   Number 6623  T       t3332   o664 b665 b3324 b3324
8547  P       p3023   Number 6646  S       s3332   t664 h
8548  O       o3023   apply p3022 p3023  G       s3332   t3332
8549  P       p3024   Number 6644  B       b3332   s3332
8550  O       o3024   apply p3022 p3024  T       t3333   o662 b3332
8551  P       p3025   Number 6642  B       b3333   t3333
8552  O       o3025   proj p3022 p3025  T       t3334   o664 b665 b3326 b3326
8553  O       o3026   uid p3022 p3025  S       s3334   t664 h
8554  T       t3026   o3026 b2524  G       s3334   t3334
8555    B       b3334   s3334
8556    T       t3335   o662 b3334
8557    B       b3335   t3335
8558    T       t3336   o620 b3326
8559    S       s3336   t671 h
8560    G       s3336   t3336
8561    B       b3336   s3336
8562    T       t3337   o662 b3336
8563    B       b3337   t3337
8564    S       s3337   t671 h
8565    G       s3337   t628
8566    B       b3338   s3337
8567    T       t3338   o662 b3338
8568    B       b3339   t3338
8569    NCzf_itt_subgroup       Czf_itt_subgroup        Czf_itt_subgroup NIL
8570    NCzf_itt_subgroup!subgroup      subgroup        subgroup Czf_itt_subgroup
8571    O       o3339   subgroup
8572    T       t3339   o3339 b3324 b576
8573    S       s3339   t671 h
8574    G       s3339   t3339
8575    B       b3340   s3339
8576    T       t3340   o662 b3340
8577    B       b3341   t3340
8578    T       t3341   o624 b3326
8579    B       b3342   t3341
8580    NCzf_itt_set_bvd        Czf_itt_set_bvd Czf_itt_set_bvd NIL
8581    NCzf_itt_set_bvd!setbvd_prop    setbvd_prop     setbvd_prop Czf_itt_set_bvd
8582    O       o3021   setbvd_prop
8583    B       b3021   t611 x
8584    T       t3021   o3021 b624 b3021
8585    B       b3022   t3021
8586    T       t3022   o3020 b2993 b576 b3022
8587    B       b3025   t3022
8588    T       t3026   o619 b480 b3025
8589  B       b3027   t3026  B       b3027   t3026
8590  P       p3027   Number 6631  T       t3027   o3019 b2997 b3027 b655 b4
 O       o3027   lid p3027 p3025  
 T       t3027   o3027 b2526  
8591  B       b3028   t3027  B       b3028   t3027
8592  T       t3028   o3025 b3027 b3028  P       p2497   Number 1929
8593  B       b3029   t3028  P       p2498   Number 1927
8594  P       p3029   Number 6643  O       o6435   location p6435 p2498
8595  O       o3029   lid p3029 p3024  T       t6435   o6435 b3028
8596  T       t3029   o3029 b2511  B       b6435   t6435
8597  B       b3030   t3029  P       p6436   Number 2180
8598  T       t3030   o3024 b3029 b3030  O       o6436   location p2497 p6436
8599  B       b3031   t3030  P       p6437   Number 1953
8600  P       p3031   Number 6645  P       p6438   Number 1961
8601  O       o3031   lid p3031 p3023  O       o6438   resource_defs p6437 p6438 p264
8602  T       t3031   o3031 b2531  P       p6439   Number 1959
8603    O       o6439   uid p6439 p6438
8604    T       t6439   o6439 b784
8605    B       b6439   t6439
8606    T       t6440   o b6439 b4
8607    B       b6440   t6440
8608    T       t6441   o6438 b6440
8609    B       b6441   t6441
8610    T       t6442   o b6441 b4
8611    B       b6442   t6442
8612    T       t6443   o659 b661 b619 b947 b6442
8613    B       b6443   t6443
8614    T       t6444   o6436 b6443
8615    B       b6444   t6444
8616    P       p6444   Number 2182
8617    P       p6445   Number 2880
8618    O       o6445   location p6444 p6445
8619    P       p6446   Number 2207
8620    P       p6447   Number 2215
8621    O       o6447   resource_defs p6446 p6447 p264
8622    P       p6448   Number 2213
8623    O       o6448   uid p6448 p6447
8624    T       t6448   o6448 b784
8625    B       b6448   t6448
8626    T       t6449   o b6448 b4
8627    B       b6449   t6449
8628    T       t6450   o6447 b6449
8629    B       b6450   t6450
8630    T       t6451   o b6450 b4
8631    B       b6451   t6451
8632    T       t6452   o792 b661 b563 b965 b6451
8633    B       b6452   t6452
8634    T       t6453   o6445 b6452
8635    B       b6453   t6453
8636    P       p6453   Number 2882
8637    P       p6454   Number 3334
8638    O       o6454   location p6453 p6454
8639    P       p6455   Number 2905
8640    P       p6456   Number 2913
8641    O       o6456   resource_defs p6455 p6456 p264
8642    P       p6457   Number 2911
8643    O       o6457   uid p6457 p6456
8644    T       t6457   o6457 b784
8645    B       b6457   t6457
8646    T       t6458   o b6457 b4
8647    B       b6458   t6458
8648    T       t6459   o6456 b6458
8649    B       b6459   t6459
8650    T       t6460   o b6459 b4
8651    B       b6460   t6460
8652    T       t6461   o10 b661 b983 b5033 b6460
8653    B       b6461   t6461
8654    T       t6462   o6454 b6461
8655    B       b6462   t6462
8656    P       p6462   Number 3336
8657    P       p6463   Number 4020
8658    O       o6463   location p6462 p6463
8659    P       p6464   Number 3365
8660    P       p6465   Number 3373
8661    O       o6465   resource_defs p6464 p6465 p264
8662    P       p6466   Number 3371
8663    O       o6466   uid p6466 p6465
8664    T       t6466   o6466 b784
8665    B       b6466   t6466
8666    T       t6467   o b6466 b4
8667    B       b6467   t6467
8668    T       t6468   o6465 b6467
8669    B       b6468   t6468
8670    T       t6469   o b6468 b4
8671    B       b6469   t6469
8672    T       t6470   o5042 b661 b2813 b5050 b6469
8673    B       b6470   t6470
8674    T       t6471   o6463 b6470
8675    B       b6471   t6471
8676    P       p6471   Number 4252
8677    P       p6472   Number 4618
8678    O       o6472   location p6471 p6472
8679    T       t6472   o6472 b1237
8680    B       b6472   t6472
8681    P       p6473   Number 4728
8682    P       p6474   Number 5144
8683    O       o6474   location p6473 p6474
8684    T       t6474   o6474 b1767
8685    B       b6474   t6474
8686    P       p6475   Number 5296
8687    P       p6476   Number 5586
8688    O       o6476   location p6475 p6476
8689    P       p6477   Number 5318
8690    P       p6478   Number 5326
8691    O       o6478   resource_defs p6477 p6478 p264
8692    P       p6479   Number 5324
8693    O       o6479   uid p6479 p6478
8694    T       t6479   o6479 b784
8695    B       b6479   t6479
8696    T       t6480   o b6479 b4
8697    B       b6480   t6480
8698    T       t6481   o6478 b6480
8699    B       b6481   t6481
8700    T       t6482   o b6481 b4
8701    B       b6482   t6482
8702    T       t6483   o2618 b3192 b4094 b2048 b6482
8703    B       b6483   t6483
8704    T       t6484   o6476 b6483
8705    B       b6484   t6484
8706    P       p6484   Number 5588
8707    P       p6485   Number 6005
8708    O       o6485   location p6484 p6485
8709    T       t6485   o6485 b2480
8710    B       b6485   t6485
8711    P       p6486   Number 6007
8712    P       p6487   Number 6088
8713    O       o6487   location p6486 p6487
8714    O       o6488   str_let p6486 p6487
8715    P       p6488   Number 6011
8716    O       o6489   patt_var p6488 p6487
8717    O       o6490   patt_done p6486 p6487
8718    T       t6490   o6490
8719    B       b6490   t6490 homIdT
8720    T       t6491   o6489 b6490
8721    B       b6491   t6491
8722    O       o6491   fun p6488 p6487
8723    O       o6492   patt_if p6488 p6487
8724    P       p6492   Number 6018
8725    P       p6493   Number 6019
8726    O       o6493   patt_var p6492 p6493
8727    O       o6494   patt_body p6488 p6487
8728    P       p6494   Number 6020
8729    P       p6495   Number 6021
8730    O       o6495   patt_var p6494 p6495
8731    P       p3100   Number 6027
8732    O       o6496   let p3100 p6487
8733    P       p6496   Number 6031
8734    P       p6497   Number 6035
8735    O       o6497   patt_tuple p6496 p6497
8736    P       p6498   Number 6032
8737    O       o6498   patt_var p6496 p6498
8738    O       o6499   patt_tuple_arg p6496 p6497
8739    P       p6499   Number 6034
8740    O       o6500   patt_var p6499 p6497
8741    O       o6501   patt_tuple_end p6496 p6497
8742    O       o6502   patt_in p3100 p6487
8743    P       p6502   Number 6071
8744    O       o6503   apply p6502 p6487
8745    P       p6503   Number 6086
8746    O       o6504   apply p6502 p6503
8747    P       p6504   Number 6084
8748    O       o6505   apply p6502 p6504
8749    P       p6505   Number 6082
8750    O       o6506   lid p6502 p6505
8751    T       t6506   o6506 b2503
8752    B       b6506   t6506
8753    P       p6506   Number 6083
8754    O       o6507   lid p6506 p6504
8755    T       t6507   o6507 b2505
8756    B       b6507   t6507
8757    T       t6508   o6505 b6506 b6507
8758    B       b6508   t6508
8759    P       p6508   Number 6085
8760    O       o6508   lid p6508 p6503
8761    T       t6509   o6508 b2508
8762    B       b6509   t6509
8763    T       t6510   o6504 b6508 b6509
8764    B       b6510   t6510
8765    P       p6510   Number 6087
8766    O       o6510   lid p6510 p6487
8767    T       t6511   o6510 b2511
8768    B       b6511   t6511
8769    T       t6512   o6503 b6510 b6511
8770    B       b6512   t6512
8771    T       t6513   o6502 b6512
8772    B       b6513   t6513
8773    T       t6514   o6501 b6513
8774    B       b6514   t6514 k
8775    T       t6515   o6500 b6514
8776    B       b6515   t6515
8777    T       t6516   o6499 b6515
8778    B       b6516   t6516 j
8779    T       t6517   o6498 b6516
8780    B       b6517   t6517
8781    T       t6518   o6497 b6517
8782    B       b6518   t6518
8783    P       p6518   Number 6038
8784    P       p6519   Number 6061
8785    O       o6519   apply p6518 p6519
8786    P       p6520   Number 6059
8787    O       o6520   apply p6518 p6520
8788    P       p6521   Number 6057
8789    O       o6521   proj p6518 p6521
8790    O       o6522   uid p6518 p6521
8791    T       t6522   o6522 b2524
8792    B       b6522   t6522
8793    P       p6522   Number 6046
8794    O       o6523   lid p6522 p6521
8795    T       t6523   o6523 b2526
8796    B       b6523   t6523
8797    T       t6524   o6521 b6522 b6523
8798    B       b6524   t6524
8799    P       p6524   Number 6058
8800    O       o6524   lid p6524 p6520
8801    T       t6525   o6524 b2511
8802    B       b6525   t6525
8803    T       t6526   o6520 b6524 b6525
8804    B       b6526   t6526
8805    P       p6526   Number 6060
8806    O       o6526   lid p6526 p6519
8807    T       t6527   o6526 b2531
8808    B       b6527   t6527
8809    T       t6528   o6519 b6526 b6527
8810    B       b6528   t6528
8811    T       t6529   o b6528 b4
8812    B       b6529   t6529
8813    T       t6530   o6496 b6518 b6529
8814    B       b6530   t6530
8815    T       t6531   o6494 b6530
8816    B       b6531   t6531 p
8817    T       t6532   o6495 b6531
8818    B       b6532   t6532
8819    T       t6533   o6492 b6532
8820    B       b6533   t6533
8821    T       t6534   o6491 b6533
8822    B       b6534   t6534
8823    T       t6535   o6494 b6534
8824    B       b6535   t6535 i
8825    T       t6536   o6493 b6535
8826    B       b6536   t6536
8827    T       t6537   o6492 b6536
8828    B       b6537   t6537
8829    T       t6538   o6491 b6537
8830    B       b6538   t6538
8831    T       t6539   o6488 b6491 b6538
8832    B       b6539   t6539
8833    T       t6540   o b6539 b4
8834    B       b6540   t6540
8835    T       t6541   o6488 b6540
8836    B       b6541   t6541
8837    T       t6542   o420 b6541
8838    B       b6542   t6542
8839    T       t6543   o6487 b6542
8840    B       b6543   t6543
8841    P       p6543   Number 6195
8842    P       p6544   Number 6597
8843    O       o6544   location p6543 p6544
8844    P       p6545   Number 6218
8845    P       p6546   Number 6226
8846    O       o6546   resource_defs p6545 p6546 p264
8847    P       p6547   Number 6224
8848    O       o6547   uid p6547 p6546
8849    T       t6547   o6547 b784
8850    B       b6547   t6547
8851    T       t6548   o b6547 b4
8852    B       b6548   t6548
8853    T       t6549   o6546 b6548
8854    B       b6549   t6549
8855    T       t6550   o b6549 b4
8856    B       b6550   t6550
8857    T       t6551   o2639 b4098 b4105 b2255 b6550
8858    B       b6551   t6551
8859    T       t6552   o6544 b6551
8860    B       b6552   t6552
8861    P       p6552   Number 6599
8862    P       p3142   Number 7316
8863    P       p3157   Number 7259
8864    O       o6552   location p6552 p3157
8865    T       t6553   o6552 b2980
8866    B       b6553   t6553
8867    P       p6553   Number 7261
8868    P       p6554   Number 7348
8869    O       o6554   location p6553 p6554
8870    O       o6555   str_let p6553 p6554
8871    P       p6555   Number 7265
8872    O       o6556   patt_var p6555 p6554
8873    O       o6557   patt_done p6553 p6554
8874    T       t6557   o6557
8875    B       b6557   t6557 homInvT
8876    T       t6558   o6556 b6557
8877    B       b6558   t6558
8878    O       o6558   fun p6555 p6554
8879    O       o6559   patt_if p6555 p6554
8880    P       p6559   Number 7273
8881    P       p6560   Number 7274
8882    O       o6560   patt_var p6559 p6560
8883    O       o6561   patt_body p6555 p6554
8884    P       p6561   Number 7275
8885    P       p6562   Number 7276
8886    O       o6562   patt_var p6561 p6562
8887    P       p6563   Number 7277
8888    P       p6564   Number 7278
8889    O       o6564   patt_var p6563 p6564
8890    P       p3161   Number 7314
8891    P       p3173   Number 7315
8892    O       o3173   lid p3173 p3142
8893    T       t3174   o3173 b2511
8894    B       b3174   t3174
8895    P       p3182   Number 7284
8896    O       o6565   let p3182 p6554
8897    P       p6565   Number 7288
8898    P       p6566   Number 7292
8899    O       o6566   patt_tuple p6565 p6566
8900    P       p6567   Number 7289
8901    O       o6567   patt_var p6565 p6567
8902    O       o6568   patt_tuple_arg p6565 p6566
8903    P       p6568   Number 7291
8904    O       o6569   patt_var p6568 p6566
8905    O       o6570   patt_tuple_end p6565 p6566
8906    O       o6571   patt_in p3182 p6554
8907    P       p6571   Number 7328
8908    O       o6572   apply p6571 p6554
8909    P       p6572   Number 7346
8910    O       o6573   apply p6571 p6572
8911    P       p6573   Number 7344
8912    O       o6574   apply p6571 p6573
8913    P       p6574   Number 7342
8914    O       o6575   apply p6571 p6574
8915    P       p6575   Number 7340
8916    O       o6576   lid p6571 p6575
8917    T       t6576   o6576 b3006
8918    B       b6576   t6576
8919    P       p6576   Number 7341
8920    O       o6577   lid p6576 p6574
8921    T       t6577   o6577 b2505
8922    B       b6577   t6577
8923    T       t6578   o6575 b6576 b6577
8924    B       b6578   t6578
8925    P       p6578   Number 7343
8926    O       o6578   lid p6578 p6573
8927    T       t6579   o6578 b2508
8928    B       b6579   t6579
8929    T       t6580   o6574 b6578 b6579
8930    B       b6580   t6580
8931    P       p6580   Number 7345
8932    O       o6580   lid p6580 p6572
8933    T       t6581   o6580 b3012
8934    B       b6581   t6581
8935    T       t6582   o6573 b6580 b6581
8936    B       b6582   t6582
8937    P       p6582   Number 7347
8938    O       o6582   lid p6582 p6554
8939    T       t6583   o6582 b2511
8940    B       b6583   t6583
8941    T       t6584   o6572 b6582 b6583
8942    B       b6584   t6584
8943    T       t6585   o6571 b6584
8944    B       b6585   t6585
8945    T       t6586   o6570 b6585
8946    B       b6586   t6586 k
8947    T       t6587   o6569 b6586
8948    B       b6587   t6587
8949    T       t6588   o6568 b6587
8950    B       b6588   t6588 j
8951    T       t6589   o6567 b6588
8952    B       b6589   t6589
8953    T       t6590   o6566 b6589
8954    B       b6590   t6590
8955    P       p6590   Number 7295
8956    P       p6591   Number 7318
8957    O       o6591   apply p6590 p6591
8958    O       o6592   apply p6590 p3142
8959    O       o6593   proj p6590 p3161
8960    O       o6594   uid p6590 p3161
8961    T       t6594   o6594 b2524
8962    B       b6594   t6594
8963    P       p6594   Number 7303
8964    O       o6595   lid p6594 p3161
8965    T       t6595   o6595 b2526
8966    B       b6595   t6595
8967    T       t6596   o6593 b6594 b6595
8968    B       b6596   t6596
8969    T       t6597   o6592 b6596 b3174
8970    B       b6597   t6597
8971    P       p6597   Number 7317
8972    O       o6597   lid p6597 p6591
8973    T       t6598   o6597 b2531
8974    B       b6598   t6598
8975    T       t6599   o6591 b6597 b6598
8976    B       b6599   t6599
8977    T       t6600   o b6599 b4
8978    B       b6600   t6600
8979    T       t6601   o6565 b6590 b6600
8980    B       b6601   t6601
8981    T       t6602   o6561 b6601
8982    B       b6602   t6602 p
8983    T       t6603   o6564 b6602
8984    B       b6603   t6603
8985    T       t6604   o6559 b6603
8986    B       b6604   t6604
8987    T       t6605   o6558 b6604
8988    B       b6605   t6605
8989    T       t6606   o6561 b6605
8990    B       b6606   t6606 i
8991    T       t6607   o6562 b6606
8992    B       b6607   t6607
8993    T       t6608   o6559 b6607
8994    B       b6608   t6608
8995    T       t6609   o6558 b6608
8996    B       b6609   t6609
8997    T       t6610   o6561 b6609
8998    B       b6610   t6610 t
8999    T       t6611   o6560 b6610
9000    B       b6611   t6611
9001    T       t6612   o6559 b6611
9002    B       b6612   t6612
9003    T       t6613   o6558 b6612
9004    B       b6613   t6613
9005    T       t6614   o6555 b6558 b6613
9006    B       b6614   t6614
9007    T       t6615   o b6614 b4
9008    B       b6615   t6615
9009    T       t6616   o6555 b6615
9010    B       b6616   t6616
9011    T       t6617   o420 b6616
9012    B       b6617   t6617
9013    T       t6618   o6554 b6617
9014    B       b6618   t6618
9015    P       p6618   Number 7472
9016    P       p6619   Number 8054
9017    O       o6619   location p6618 p6619
9018    NCzf_itt_set_bvd!set_bvd        set_bvd set_bvd Czf_itt_set_bvd
9019    O       o3342   set_bvd
9020    T       t3342   o624 b3324
9021    B       b3343   t3342
9022    T       t3343   o3342 b3343 b582
9023    B       b3344   t3343
9024    T       t3695   o3020 b3326 b577 b3344
9025    S       s3695   t671 h
9026    G       s3695   t3695
9027    B       b3695   s3695
9028    T       t3696   o662 b3695
9029    B       b3696   t3696
9030    T       t3344   o952 b3342 b3344
9031    S       s3344   t671 h
9032    G       s3344   t3344
9033    B       b3345   s3344
9034    T       t3346   o629 b409 b3342
9035    H       h3346   x1 t3346
9036    T       t3347   o629 b411 b3342
9037    H       h3347   y1 t3347
9038    T       t3348   o532 b3326
9039    B       b3348   t3348
9040    T       t3349   o637 b3326 b409 b411
9041    B       b3349   t3349
9042    T       t3350   o637 b577 b409 b411
9043    B       b3350   t3350
9044    T       t3351   o623 b3342 b3348 b3349 b3350
9045    S       s3351   t671 h h408 h409 h3346 h3347
9046    G       s3351   t3351
9047    B       b3351   s3351
9048    T       t3353   o623 b3342 b3348 b519 b526
9049    H       h3353   v t3353
9050    T       t3354   o623 b626 b537 b519 b526
9051    S       s3354   t671 h h518 h519 h3353
9052    G       s3354   t3354
9053    B       b3354   s3354
9054    H       h3355   p t634
9055    H       h3356   q t634
9056    T       t3356   o629 b2511 b3342
9057    H       h3357   x2 t3356
9058    P       p3357   Var q
9059    O       o3357   var p3357
9060    T       t3357   o3357
9061    B       b3357   t3357
9062    T       t3358   o629 b3357 b3342
9063    H       h3358   y2 t3358
9064    T       t3359   o623 b626 b537 b2511 b3357
9065    H       h3359   w t3359
9066    T       t3360   o623 b3342 b3348 b2511 b3357
9067    S       s3360   t671 h h3355 h3356 h3357 h3358 h3359
9068    G       s3360   t3360
9069    B       b3360   s3360
9070    T       t3362   o3339 b3326 b577
9071    S       s3362   t671 h
9072    G       s3362   t3362
9073    B       b3362   s3362
9074    T       t3363   o662 b3362
9075    B       b3363   t3363
9076    T       t3697   o661 b3696 b3363
9077    B       b3697   t3697
9078    T       t3698   o661 b3341 b3697
9079    B       b3698   t3698
9080    T       t3699   o661 b2708 b3698
9081    B       b3699   t3699
9082    T       t3700   o661 b3339 b3699
9083    B       b3700   t3700
9084    T       t3701   o661 b3337 b3700
9085    B       b3701   t3701
9086    T       t3702   o661 b3335 b3701
9087    B       b3702   t3702
9088    T       t3703   o661 b3333 b3702
9089    B       b3703   t3703
9090    T       t3704   o661 b669 b3703
9091    B       b3704   t3704
9092    T       t3705   o661 b667 b3704
9093    B       b3705   t3705
9094    P       p3705   String "assumT 7 thenT assumT 9 thenT rwh unfold_hom 2 thenT rwh unfold_group_bvd 3 thenT autoT"
9095    O       o3705   ext_rule p3705
9096    T       t3706   o b3695 b4
9097    B       b3706   t3706
9098    T       t3707   o b3340 b3706
9099    B       b3707   t3707
9100    T       t3708   o b2707 b3707
9101    B       b3708   t3708
9102    T       t3709   o b3338 b3708
9103    B       b3709   t3709
9104    T       t3710   o b3336 b3709
9105    B       b3710   t3710
9106    T       t3711   o b3334 b3710
9107    B       b3711   t3711
9108    T       t3712   o b3332 b3711
9109    B       b3712   t3712
9110    T       t3713   o b668 b3712
9111    B       b3713   t3713
9112    T       t3714   o b666 b3713
9113    B       b3714   t3714
9114    T       t3715   o695 b3362 b3714
9115    B       b3715   t3715
9116    T       t3716   o694 b3715 b4 b703
9117    B       b3716   t3716
9118    H       h3716   y_6 t620
9119    H       h3717   y_7 t621
9120    H       h3718   y_8 t530
9121    H       h3719   y_9 t269
9122    H       h3720   y t3336
9123    T       t3720   o621 b3344
9124    H       h3721   y_2 t3720
9125    H       h3722   y_3 t3344
9126    T       t3722   o629 b630 b3342
9127    B       b3722   t3722
9128    T       t3723   o629 b636 b3342
9129    B       b3723   t3723
9130    T       t3724   o637 b3326 b630 b636
9131    B       b3724   t3724
9132    T       t3725   o623 b3342 b3348 b3724 b1142
9133    B       b3725   t3725
9134    T       t3726   o635 b3723 b3725
9135    B       b3726   t3726
9136    T       t3727   o635 b3722 b3726
9137    B       b3727   t3727 b
9138    T       t3728   o633 b634 b3727
9139    B       b3728   t3728 a
9140    T       t3729   o633 b634 b3728
9141    H       h3729   y_4 t3729
9142    T       t3730   o623 b3342 b3348 b630 b636
9143    B       b3730   t3730
9144    T       t3731   o623 b626 b537 b630 b636
9145    B       b3731   t3731
9146    T       t3732   o635 b3730 b3731
9147    B       b3732   t3732 b
9148    T       t3733   o633 b634 b3732
9149    B       b3733   t3733 a
9150    T       t3734   o633 b634 b3733
9151    H       h3734   y_5 t3734
9152    T       t3735   o635 b3731 b3730
9153    B       b3735   t3735
9154    T       t3736   o635 b3723 b3735
9155    B       b3736   t3736
9156    T       t3737   o635 b3722 b3736
9157    B       b3737   t3737 b
9158    T       t3738   o633 b634 b3737
9159    B       b3738   t3738 a
9160    T       t3739   o633 b634 b3738
9161    H       h3739   z_1 t3739
9162    T       t3376   o b3360 b4
9163    B       b3376   t3376
9164    T       t3377   o b3354 b3376
9165    B       b3377   t3377
9166    T       t3378   o b3351 b3377
9167    B       b3378   t3378
9168    T       t3379   o b3345 b3378
9169    B       b3379   t3379
9170    T       t3380   o b3340 b3379
9171    B       b3380   t3380
9172    T       t3381   o b2707 b3380
9173    B       b3381   t3381
9174    T       t3382   o b3338 b3381
9175    B       b3382   t3382
9176    T       t3383   o b3336 b3382
9177    B       b3383   t3383
9178    T       t3384   o b3334 b3383
9179    B       b3384   t3384
9180    T       t3385   o b3332 b3384
9181    B       b3385   t3385
9182    T       t3386   o b668 b3385
9183    B       b3386   t3386
9184    T       t3387   o b666 b3386
9185    B       b3387   t3387
9186    T       t3388   o695 b3362 b3387
9187    B       b3388   t3388
9188    T       t3389   o694 b3388 b4 b703
9189    B       b3389   t3389
9190    H       h3389   v_1 t3344
9191    T       t3390   o629 b581 b3342
9192    H       h3390   y t3390
9193    S       s3739   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390
9194    G       s3739   t407
9195    B       b3739   s3739
9196    T       t3740   o695 b3739 b3714
9197    B       b3740   t3740
9198    T       t3391   o629 b581 b3344
9199    H       h3391   x t3391
9200    T       t3392   o621 b785
9201    S       s3392   t664 h h1033 h1034 h1769 h1770 h1771 h3389 h678 h3390 h3391 h911
9202    G       s3392   t3392
9203    B       b3392   s3392
9204    T       t3393   o695 b3392 b3387
9205    B       b3393   t3393
9206    H       h3393   v t3391
9207    S       s3393   t671 h h1033 h1034 h1769 h1770 h1771 h3389 h678 h3390 h3393
9208    G       s3393   t407
9209    B       b3394   s3393
9210    T       t3394   o695 b3394 b3387
9211    B       b3395   t3394
9212    S       s3395   t671 h h1033 h1034 h1769 h1770 h1771 h3389 h678 h3390
9213    G       s3395   t407
9214    B       b3396   s3395
9215    T       t3396   o695 b3396 b3387
9216    B       b3397   t3396
9217    NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL
9218    NCzf_itt_subset!subset  subset  subset Czf_itt_subset
9219    O       o3397   subset
9220    T       t3397   o3397 b3342 b626
9221    S       s3740   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9222    G       s3740   t3397
9223    B       b3741   s3740
9224    T       t3741   o695 b3741 b3714
9225    B       b3742   t3741
9226    S       s3742   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9227    G       s3742   t3362
9228    B       b3743   s3742
9229    T       t3743   o695 b3743 b3714
9230    B       b3744   t3743
9231    S       s3744   t671 h h3716 h3717 h3718 h1772 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9232    G       s3744   t3362
9233    B       b3745   s3744
9234    T       t3745   o695 b3745 b3714
9235    B       b3746   t3745
9236    S       s3746   t671 h h3716 h3717 h1276 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9237    G       s3746   t3362
9238    B       b3747   s3746
9239    T       t3747   o695 b3747 b3714
9240    B       b3748   t3747
9241    S       s3748   t671 h h3716 h1776 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9242    G       s3748   t3362
9243    B       b3749   s3748
9244    T       t3749   o695 b3749 b3714
9245    B       b3750   t3749
9246    S       s3750   t671 h h1778 h3720 h1034 h3721 h3722 h3729 h3734 h3739
9247    G       s3750   t3362
9248    B       b3751   s3750
9249    T       t3751   o695 b3751 b3714
9250    B       b3752   t3751
9251    B       b3753   t3734
9252    B       b3754   t3739
9253    T       t3754   o619 b3753 b3754
9254    H       h3754   z t3754
9255    S       s3754   t671 h h1778 h3720 h1034 h3721 h3722 h3729 h3754
9256    G       s3754   t3362
9257    B       b3755   s3754
9258    T       t3755   o695 b3755 b3714
9259    B       b3756   t3755
9260    B       b3757   t3729
9261    B       b3758   t3754
9262    T       t3758   o619 b3757 b3758
9263    H       h3758   z_1 t3758
9264    S       s3758   t671 h h1778 h3720 h1034 h3721 h3722 h3758
9265    G       s3758   t3362
9266    B       b3759   s3758
9267    T       t3759   o695 b3759 b3714
9268    B       b3760   t3759
9269    B       b3761   t3344
9270    B       b3762   t3758
9271    T       t3762   o619 b3761 b3762
9272    H       h3762   z t3762
9273    S       s3762   t671 h h1778 h3720 h1034 h3721 h3762
9274    G       s3762   t3362
9275    B       b3763   s3762
9276    T       t3763   o695 b3763 b3714
9277    B       b3764   t3763
9278    B       b3765   t3720
9279    B       b3766   t3762
9280    T       t3766   o619 b3765 b3766
9281    H       h3766   z_1 t3766
9282    S       s3766   t671 h h1778 h3720 h1034 h3766
9283    G       s3766   t3362
9284    B       b3767   s3766
9285    T       t3767   o695 b3767 b3714
9286    B       b3768   t3767
9287    B       b3769   t3766
9288    T       t3769   o619 b621 b3769
9289    H       h3769   z t3769
9290    S       s3769   t671 h h1778 h3720 h3769
9291    G       s3769   t3362
9292    B       b3770   s3769
9293    T       t3770   o695 b3770 b3714
9294    B       b3771   t3770
9295    B       b3772   t3336
9296    B       b3773   t3769
9297    T       t3773   o619 b3772 b3773
9298    H       h3773   v_1 t3773
9299    S       s3773   t671 h h1778 h3773
9300    G       s3773   t3362
9301    B       b3774   s3773
9302    T       t3774   o695 b3774 b3714
9303    B       b3775   t3774
9304    H       h3775   v_1 t3695
9305    S       s3775   t671 h h1778 h3775
9306    G       s3775   t3362
9307    B       b3776   s3775
9308    T       t3776   o695 b3776 b3714
9309    B       b3777   t3776
9310    S       s3777   t671 h h1780 h3775
9311    G       s3777   t3362
9312    B       b3778   s3777
9313    T       t3778   o695 b3778 b3714
9314    B       b3779   t3778
9315    S       s3397   t671 h h1033 h1034 h1769 h1770 h1771 h3389
9316    G       s3397   t3397
9317    B       b3398   s3397
9318    T       t3398   o695 b3398 b3387
9319    B       b3399   t3398
9320    S       s3399   t671 h h1033 h1034 h1769 h1770 h1771 h3389
9321    G       s3399   t3362
9322    B       b3400   s3399
9323    T       t3400   o695 b3400 b3387
9324    B       b3401   t3400
9325    S       s3401   t671 h h1033 h1034 h1769 h1772 h3389
9326    G       s3401   t3362
9327    B       b3402   s3401
9328    T       t3402   o695 b3402 b3387
9329    B       b3403   t3402
9330    S       s3403   t671 h h1033 h1034 h1774 h3389
9331    G       s3403   t3362
9332    B       b3404   s3403
9333    T       t3404   o695 b3404 b3387
9334    B       b3405   t3404
9335    S       s3405   t671 h h1033 h1776 h3389
9336    G       s3405   t3362
9337    B       b3406   s3405
9338    T       t3406   o695 b3406 b3387
9339    B       b3407   t3406
9340    S       s3407   t671 h h1778 h3389
9341    G       s3407   t3362
9342    B       b3408   s3407
9343    T       t3408   o695 b3408 b3387
9344    B       b3409   t3408
9345    S       s3409   t671 h h1780 h3389
9346    G       s3409   t3362
9347    B       b3410   s3409
9348    T       t3410   o695 b3410 b3387
9349    B       b3411   t3410
9350    S       s3411   t671 h h1780
9351    G       s3411   t3362
9352    B       b3412   s3411
9353    T       t3779   o695 b3412 b3714
9354    B       b3780   t3779
9355    T       t3780   o2 b3716
9356    B       b3781   t3780
9357    T       t3781   o694 b3780 b4 b3781
9358    B       b3782   t3781
9359    T       t3782   o2 b3782
9360    B       b3783   t3782
9361    T       t3783   o694 b3779 b4 b3783
9362    B       b3784   t3783
9363    T       t3784   o2 b3784
9364    B       b3785   t3784
9365    T       t3785   o694 b3777 b4 b3785
9366    B       b3786   t3785
9367    T       t3786   o2 b3786
9368    B       b3787   t3786
9369    T       t3787   o694 b3775 b4 b3787
9370    B       b3788   t3787
9371    T       t3788   o2 b3788
9372    B       b3789   t3788
9373    T       t3789   o694 b3771 b4 b3789
9374    B       b3790   t3789
9375    T       t3790   o2 b3790
9376    B       b3791   t3790
9377    T       t3791   o694 b3768 b4 b3791
9378    B       b3792   t3791
9379    T       t3792   o2 b3792
9380    B       b3793   t3792
9381    T       t3793   o694 b3764 b4 b3793
9382    B       b3794   t3793
9383    T       t3794   o2 b3794
9384    B       b3795   t3794
9385    T       t3795   o694 b3760 b4 b3795
9386    B       b3796   t3795
9387    T       t3796   o2 b3796
9388    B       b3797   t3796
9389    T       t3797   o694 b3756 b4 b3797
9390    B       b3798   t3797
9391    T       t3798   o2 b3798
9392    B       b3799   t3798
9393    T       t3799   o694 b3752 b4 b3799
9394    B       b3800   t3799
9395    T       t3800   o2 b3800
9396    B       b3801   t3800
9397    T       t3801   o694 b3750 b4 b3801
9398    B       b3802   t3801
9399    T       t3802   o2 b3802
9400    B       b3803   t3802
9401    T       t3803   o694 b3748 b4 b3803
9402    B       b3804   t3803
9403    T       t3804   o2 b3804
9404    B       b3805   t3804
9405    T       t3805   o694 b3746 b4 b3805
9406    B       b3806   t3805
9407    T       t3806   o2 b3806
9408    B       b3807   t3806
9409    T       t3807   o694 b3744 b711 b3807
9410    B       b3808   t3807
9411    T       t3808   o2 b3808
9412    B       b3809   t3808
9413    T       t3809   o694 b3742 b711 b3809
9414    B       b3810   t3809
9415    T       t3810   o2 b3810
9416    B       b3811   t3810
9417    T       t3811   o694 b3740 b4 b3811
9418    B       b3812   t3811
9419    T       t3812   o b3812 b4
9420    B       b3813   t3812
9421    T       t3813   o693 b3716 b3813
9422    B       b3814   t3813
9423    P       p3814   String "setSubstT << equal{car{'h2}; set_bvd{car{'h1}; x. 'f['x]}} >> 15 ttca thenT dT 16 ttca"
9424    O       o3814   ext_rule p3814
9425    S       s3814   t664 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911
9426    G       s3814   t3392
9427    B       b3815   s3814
9428    T       t3815   o695 b3815 b3714
9429    B       b3816   t3815
9430    S       s3816   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3393
9431    G       s3816   t407
9432    B       b3817   s3816
9433    T       t3817   o695 b3817 b3714
9434    B       b3818   t3817
9435    T       t3818   o2 b3812
9436    B       b3819   t3818
9437    T       t3819   o694 b3818 b4 b3819
9438    B       b3820   t3819
9439    T       t3820   o2 b3820
9440    B       b3821   t3820
9441    T       t3821   o694 b3816 b4 b3821
9442    B       b3822   t3821
9443    T       t3412   o695 b3412 b3387
9444    B       b3413   t3412
9445    T       t3413   o2 b3389
9446    B       b3414   t3413
9447    T       t3414   o694 b3413 b4 b3414
9448    B       b3415   t3414
9449    T       t3415   o2 b3415
9450    B       b3416   t3415
9451    T       t3416   o694 b3411 b4 b3416
9452    B       b3417   t3416
9453    T       t3417   o2 b3417
9454    B       b3418   t3417
9455    T       t3418   o694 b3409 b4 b3418
9456    B       b3419   t3418
9457    T       t3419   o2 b3419
9458    B       b3420   t3419
9459    T       t3420   o694 b3407 b4 b3420
9460    B       b3421   t3420
9461    T       t3421   o2 b3421
9462    B       b3422   t3421
9463    T       t3422   o694 b3405 b4 b3422
9464    B       b3423   t3422
9465    T       t3423   o2 b3423
9466    B       b3424   t3423
9467    T       t3424   o694 b3403 b4 b3424
9468    B       b3425   t3424
9469    T       t3425   o2 b3425
9470    B       b3426   t3425
9471    T       t3426   o694 b3401 b711 b3426
9472    B       b3427   t3426
9473    T       t3427   o2 b3427
9474    B       b3428   t3427
9475    T       t3428   o694 b3399 b711 b3428
9476    B       b3429   t3428
9477    T       t3429   o2 b3429
9478    B       b3430   t3429
9479    T       t3430   o694 b3397 b4 b3430
9480    B       b3431   t3430
9481    T       t3431   o2 b3431
9482    B       b3432   t3431
9483    T       t3432   o694 b3395 b4 b3432
9484    B       b3433   t3432
9485    T       t3433   o2 b3433
9486    B       b3434   t3433
9487    T       t3434   o694 b3393 b4 b3434
9488    B       b3435   t3434
9489    T       t3435   o629 b793 b3343
9490    H       h3435   u t3435
9491    T       t3436   o1049 b581 b785
9492    H       h3436   v t3436
9493    S       s3822   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436
9494    G       s3822   t407
9495    B       b3823   s3822
9496    T       t3823   o695 b3823 b3714
9497    B       b3824   t3823
9498    T       t3824   o694 b3824 b4 b3821
9499    B       b3825   t3824
9500    T       t3825   o b3825 b4
9501    B       b3826   t3825
9502    T       t3826   o b3822 b3826
9503    B       b3827   t3826
9504    T       t3827   o693 b3812 b3827
9505    B       b3828   t3827
9506    P       p3828   String "funSetT 17 ttca"
9507    O       o3828   ext_rule p3828
9508    T       t3828   o693 b3822 b4
9509    B       b3829   t3828
9510    T       t3829   o3828 b692 b3829 b4 b4
9511    B       b3830   t3829
9512    P       p3830   String "withT << 'z >> (dT 4) ttca thenT dT 19 ttca"
9513    O       o3830   ext_rule p3830
9514    S       s3830   t671 h h3716 h3717 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436
9515    G       s3830   t615
9516    B       b3831   s3830
9517    T       t3831   o695 b3831 b3714
9518    B       b3832   t3831
9519    S       s3436   t671 h h1033 h1034 h1769 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436
9520    G       s3436   t407
9521    B       b3436   s3436
9522    T       t3437   o695 b3436 b3387
9523    B       b3437   t3437
9524    T       t3438   o694 b3437 b4 b3434
9525    B       b3438   t3438
9526    P       p3441   String "funSetT 11 ttca"
9527    O       o3441   ext_rule p3441
9528    T       t3442   o693 b3435 b4
9529    B       b3442   t3442
9530    T       t3443   o3441 b692 b3442 b4 b4
9531    B       b3443   t3443
9532    P       p3443   String "withT << 'z >> (dT 4) ttca thenT dT 13 ttca"
9533    O       o3443   ext_rule p3443
9534    S       s3443   t671 h h1033 h1034 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436
9535    G       s3443   t615
9536    B       b3444   s3443
9537    T       t3444   o695 b3444 b3387
9538    B       b3445   t3444
9539    T       t3445   o629 b785 b626
9540    B       b3446   t3445
9541    T       t3446   o635 b615 b3446
9542    H       h3446   w t3446
9543    S       s3832   t671 h h3716 h3717 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436 h3446
9544    G       s3832   t615
9545    B       b3833   s3832
9546    T       t3833   o695 b3833 b3714
9547    B       b3834   t3833
9548    S       s3834   t671 h h3716 h3717 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436 h3446
9549    G       s3834   t407
9550    B       b3835   s3834
9551    T       t3835   o695 b3835 b3714
9552    B       b3836   t3835
9553    S       s3836   t671 h h3716 h3717 h3718 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436 h3446
9554    G       s3836   t407
9555    B       b3837   s3836
9556    T       t3837   o695 b3837 b3714
9557    B       b3838   t3837
9558    S       s3446   t671 h h1033 h1034 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436 h3446
9559    G       s3446   t615
9560    B       b3447   s3446
9561    T       t3447   o695 b3447 b3387
9562    B       b3448   t3447
9563    S       s3448   t671 h h1033 h1034 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436 h3446
9564    G       s3448   t407
9565    B       b3449   s3448
9566    T       t3449   o695 b3449 b3387
9567    B       b3450   t3449
9568    S       s3450   t671 h h1033 h1034 h1769 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436 h3446
9569    G       s3450   t407
9570    B       b3451   s3450
9571    T       t3451   o695 b3451 b3387
9572    B       b3452   t3451
9573    T       t3452   o b793 b4
9574    B       b3453   t3452
9575    T       t3453   o1207 b3453
9576    B       b3454   t3453
9577    T       t3454   o1206 b3454
9578    B       b3455   t3454
9579    T       t3455   o b3455 b4
9580    B       b3456   t3455
9581    T       t3838   o694 b3824 b3456 b3821
9582    B       b3839   t3838
9583    T       t3839   o2 b3839
9584    B       b3840   t3839
9585    T       t3840   o694 b3838 b3456 b3840
9586    B       b3841   t3840
9587    T       t3841   o2 b3841
9588    B       b3842   t3841
9589    T       t3842   o694 b3836 b4 b3842
9590    B       b3843   t3842
9591    T       t3843   o2 b3843
9592    B       b3844   t3843
9593    T       t3844   o2266 b3834 b4 b3844
9594    B       b3845   t3844
9595    T       t3845   o2 b3845
9596    B       b3846   t3845
9597    T       t3846   o2266 b3832 b4 b3846
9598    B       b3847   t3846
9599    H       h3847   y_8 t3445
9600    S       s3847   t671 h h3716 h3717 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436 h3847
9601    G       s3847   t407
9602    B       b3848   s3847
9603    T       t3848   o695 b3848 b3714
9604    B       b3849   t3848
9605    S       s3849   t671 h h3716 h3717 h3719 h941 h3720 h1034 h3721 h3722 h3729 h3734 h3739 h678 h3390 h3391 h911 h3435 h3436 h3446 h3847
9606    G       s3849   t407
9607    B       b3850   s3849
9608    T       t3850   o695 b3850 b3714
9609    B       b3851   t3850
9610    T       t3851   o694 b3851 b4 b3844
9611    B       b3852   t3851
9612    T       t3852   o2 b3852
9613    B       b3853   t3852
9614    T       t3853   o694 b3849 b4 b3853
9615    B       b3854   t3853
9616    T       t3854   o b3854 b4
9617    B       b3855   t3854
9618    T       t3855   o b3847 b3855
9619    B       b3856   t3855
9620    T       t3856   o693 b3825 b3856
9621    B       b3857   t3856
9622    P       p3857   String "assumT 8 thenT rwh unfold_subgroup 19 thenT autoT thenT withT << 'z >> (dT 21) ttca"
9623    O       o3857   ext_rule p3857
9624    T       t3857   o693 b3847 b4
9625    B       b3858   t3857
9626    T       t3858   o3857 b692 b3858 b4 b4
9627    B       b3859   t3858
9628    P       p3859   String "setSubstT << equal{'x; 'f['z]} >> 0 thenT autoT thenT funSetT 16 ttca"
9629    O       o3859   ext_rule p3859
9630    T       t3859   o693 b3854 b4
9631    B       b3860   t3859
9632    T       t3860   o3859 b692 b3860 b4 b4
9633    B       b3861   t3860
9634    T       t3861   o b3861 b4
9635    B       b3862   t3861
9636    T       t3862   o b3859 b3862
9637    B       b3863   t3862
9638    T       t3863   o3830 b692 b3857 b3863 b4
9639    B       b3864   t3863
9640    T       t3866   o b3864 b4
9641    B       b3866   t3866
9642    T       t3867   o b3830 b3866
9643    B       b3867   t3867
9644    T       t3868   o3814 b692 b3828 b3867 b4
9645    B       b3868   t3868
9646    T       t3869   o b3868 b4
9647    B       b3869   t3869
9648    T       t3456   o694 b3437 b3456 b3434
9649    B       b3457   t3456
9650    T       t3457   o2 b3457
9651    B       b3458   t3457
9652    T       t3458   o694 b3452 b3456 b3458
9653    B       b3459   t3458
9654    T       t3459   o2 b3459
9655    B       b3460   t3459
9656    T       t3460   o694 b3450 b4 b3460
9657    B       b3461   t3460
9658    T       t3461   o2 b3461
9659    B       b3462   t3461
9660    T       t3462   o2266 b3448 b4 b3462
9661    B       b3463   t3462
9662    T       t3463   o2 b3463
9663    B       b3464   t3463
9664    T       t3464   o2266 b3445 b4 b3464
9665    B       b3465   t3464
9666    H       h3465   y_2 t3445
9667    S       s3465   t671 h h1033 h1034 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436 h3465
9668    G       s3465   t407
9669    B       b3466   s3465
9670    T       t3466   o695 b3466 b3387
9671    B       b3467   t3466
9672    S       s3467   t671 h h1033 h1034 h1770 h1771 h3389 h678 h3390 h3391 h911 h3435 h3436 h3446 h3465
9673    G       s3467   t407
9674    B       b3468   s3467
9675    T       t3468   o695 b3468 b3387
9676    B       b3469   t3468
9677    T       t3469   o694 b3469 b4 b3462
9678    B       b3470   t3469
9679    T       t3470   o2 b3470
9680    B       b3471   t3470
9681    T       t3471   o694 b3467 b4 b3471
9682    B       b3472   t3471
9683    T       t3472   o b3472 b4
9684    B       b3473   t3472
9685    T       t3473   o b3465 b3473
9686    B       b3474   t3473
9687    T       t3474   o693 b3438 b3474
9688    B       b3475   t3474
9689    P       p3475   String "assumT 8 thenT rwh unfold_subgroup 13 thenT autoT thenT withT << 'z >> (dT 15) ttca"
9690    O       o3475   ext_rule p3475
9691    T       t3475   o693 b3465 b4
9692    B       b3476   t3475
9693    T       t3476   o3475 b692 b3476 b4 b4
9694    B       b3477   t3476
9695    P       p3477   String "setSubstT << equal{'x; 'f['z]} >> 0 thenT autoT thenT funSetT 10 ttca"
9696    O       o3477   ext_rule p3477
9697    T       t3477   o693 b3472 b4
9698    B       b3478   t3477
9699    T       t3478   o3477 b692 b3478 b4 b4
9700    B       b3479   t3478
9701    T       t3479   o b3479 b4
9702    B       b3480   t3479
9703    T       t3480   o b3477 b3480
9704    B       b3481   t3480
9705    T       t3481   o3443 b692 b3475 b3481 b4
9706    B       b3482   t3481
9707    T       t3482   o b3482 b4
9708    B       b3483   t3482
9709    T       t3483   o b3443 b3483
9710    B       b3484   t3483
9711    T       t3870   o3705 b692 b3814 b3869 b3484
9712    B       b3870   t3870
9713    T       t3871   o690 b3870
9714    B       b3871   t3871
9715    T       t3872   o3323 b3331 b3705 b3871 b4
9716    B       b3872   t3872
9717    T       t6619   o6619 b3872
9718    B       b6619   t6619
9719    P       p6620   Number 8199
9720    P       p6621   Number 8793
9721    O       o6621   location p6620 p6621
9722    P       p3227   String hom_subgroup2
9723    O       o3227   rule p3227
9724    T       t3227   o620 b3324
9725    S       s3227   t671 h
9726    G       s3227   t3227
9727    B       b3227   s3227
9728    T       t3228   o662 b3227
9729    B       b3228   t3228
9730    NCzf_itt_inv_image      Czf_itt_inv_image       Czf_itt_inv_image NIL
9731    NCzf_itt_inv_image!inv_image    inv_image       inv_image Czf_itt_inv_image
9732    O       o3228   inv_image
9733    T       t3229   o3228 b624 b582 b3342
9734    B       b3229   t3229
9735    T       t3230   o3020 b3324 b576 b3229
9736    S       s3230   t671 h
9737    G       s3230   t3230
9738    B       b3230   s3230
9739    T       t3231   o662 b3230
9740    B       b3231   t3231
9741    T       t3232   o661 b3231 b3341
9742    B       b3232   t3232
9743    T       t3233   o661 b3363 b3232
9744    B       b3233   t3233
9745    T       t3234   o661 b2708 b3233
9746    B       b3234   t3234
9747    T       t3235   o661 b3339 b3234
9748    B       b3235   t3235
9749    T       t3236   o661 b3228 b3235
9750    B       b3236   t3236
9751    T       t3237   o661 b3335 b3236
9752    B       b3237   t3237
9753    T       t3238   o661 b3333 b3237
9754    B       b3238   t3238
9755    T       t3239   o661 b669 b3238
9756    B       b3239   t3239
9757    T       t3240   o661 b667 b3239
9758    B       b3240   t3240
9759    P       p3240   String "assumT 7 thenT assumT 8 thenT assumT 9 thenT rwh unfold_hom 2 thenT rwh unfold_group_bvd 4 thenT autoT"
9760    O       o3240   ext_rule p3240
9761    T       t3241   o b3230 b4
9762    B       b3241   t3241
9763    T       t3242   o b3362 b3241
9764    B       b3242   t3242
9765    T       t3243   o b2707 b3242
9766    B       b3243   t3243
9767    T       t3247   o b3338 b3243
9768    B       b3247   t3247
9769    T       t3248   o b3227 b3247
9770    B       b3248   t3248
9771    T       t3249   o b3334 b3248
9772    B       b3249   t3249
9773    T       t3250   o b3332 b3249
9774    B       b3250   t3250
9775    T       t3251   o b668 b3250
9776    B       b3251   t3251
9777    T       t3252   o b666 b3251
9778    B       b3252   t3252
9779    T       t3253   o695 b3340 b3252
9780    B       b3253   t3253
9781    T       t3258   o694 b3253 b4 b703
9782    B       b3258   t3258
9783    H       h3258   v_1 t3362
9784    H       h3259   y t3227
9785    T       t3259   o621 b3229
9786    H       h3260   y_2 t3259
9787    T       t3270   o952 b3343 b3229
9788    H       h3270   y_3 t3270
9789    T       t3271   o629 b630 b3343
9790    B       b3271   t3271
9791    T       t3272   o629 b636 b3343
9792    B       b3272   t3272
9793    T       t3273   o532 b3324
9794    B       b3273   t3273
9795    T       t3274   o637 b3324 b630 b636
9796    B       b3274   t3274
9797    T       t3275   o623 b3343 b3273 b3274 b638
9798    B       b3275   t3275
9799    T       t3276   o635 b3272 b3275
9800    B       b3276   t3276
9801    T       t3277   o635 b3271 b3276
9802    B       b3277   t3277 b
9803    T       t3278   o633 b634 b3277
9804    B       b3278   t3278 a
9805    T       t3279   o633 b634 b3278
9806    H       h3279   y_4 t3279
9807    T       t3280   o623 b3343 b3273 b630 b636
9808    B       b3280   t3280
9809    T       t3281   o635 b3280 b3875
9810    B       b3281   t3281 b
9811    T       t3282   o633 b634 b3281
9812    B       b3282   t3282 a
9813    T       t3283   o633 b634 b3282
9814    H       h3283   y_5 t3283
9815    T       t3284   o635 b3875 b3280
9816    B       b3284   t3284
9817    T       t3285   o635 b3272 b3284
9818    B       b3285   t3285
9819    T       t3286   o635 b3271 b3285
9820    B       b3286   t3286 b
9821    T       t3287   o633 b634 b3286
9822    B       b3287   t3287 a
9823    T       t3288   o633 b634 b3287
9824    H       h3288   z_1 t3288
9825    T       t3289   o629 b581 b3343
9826    H       h3289   y t3289
9827    S       s3289   t671 h h3716 h3717 h3718 h3719 h941 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288 h678 h3289
9828    G       s3289   t797
9829    B       b3289   s3289
9830    T       t3290   o695 b3289 b3252
9831    B       b3290   t3290
9832    T       t3291   o3397 b3343 b624
9833    S       s3291   t671 h h3716 h3717 h3718 h3719 h941 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9834    G       s3291   t3291
9835    B       b3291   s3291
9836    T       t3292   o695 b3291 b3252
9837    B       b3292   t3292
9838    S       s3292   t671 h h3716 h3717 h3718 h3719 h941 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9839    G       s3292   t3339
9840    B       b3296   s3292
9841    T       t3296   o695 b3296 b3252
9842    B       b3297   t3296
9843    S       s3297   t671 h h3716 h3717 h3718 h1772 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9844    G       s3297   t3339
9845    B       b3298   s3297
9846    T       t3298   o695 b3298 b3252
9847    B       b3299   t3298
9848    S       s3299   t671 h h3716 h3717 h1276 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9849    G       s3299   t3339
9850    B       b3300   s3299
9851    T       t3300   o695 b3300 b3252
9852    B       b3301   t3300
9853    S       s3301   t671 h h3716 h1776 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9854    G       s3301   t3339
9855    B       b3302   s3301
9856    T       t3302   o695 b3302 b3252
9857    B       b3303   t3302
9858    S       s3303   t671 h h1778 h3258 h3259 h937 h3260 h3270 h3279 h3283 h3288
9859    G       s3303   t3339
9860    B       b3304   s3303
9861    T       t3304   o695 b3304 b3252
9862    B       b3305   t3304
9863    B       b3306   t3283
9864    B       b3307   t3288
9865    T       t3307   o619 b3306 b3307
9866    H       h3307   z t3307
9867    S       s3307   t671 h h1778 h3258 h3259 h937 h3260 h3270 h3279 h3307
9868    G       s3307   t3339
9869    B       b3308   s3307
9870    T       t3308   o695 b3308 b3252
9871    B       b3309   t3308
9872    B       b3310   t3279
9873    B       b3311   t3307
9874    T       t3311   o619 b3310 b3311
9875    H       h3311   z_1 t3311
9876    S       s3311   t671 h h1778 h3258 h3259 h937 h3260 h3270 h3311
9877    G       s3311   t3339
9878    B       b3312   s3311
9879    T       t3312   o695 b3312 b3252
9880    B       b3313   t3312
9881    B       b3314   t3270
9882    B       b3315   t3311
9883    T       t3315   o619 b3314 b3315
9884    H       h3315   z t3315
9885    S       s3315   t671 h h1778 h3258 h3259 h937 h3260 h3315
9886    G       s3315   t3339
9887    B       b3316   s3315
9888    T       t3316   o695 b3316 b3252
9889    B       b3317   t3316
9890    B       b3318   t3259
9891    B       b3319   t3315
9892    T       t3319   o619 b3318 b3319
9893    H       h3319   z_1 t3319
9894    S       s3319   t671 h h1778 h3258 h3259 h937 h3319
9895    G       s3319   t3339
9896    B       b3320   s3319
9897    T       t3320   o695 b3320 b3252
9898    B       b3321   t3320
9899    B       b3346   t3319
9900    T       t3352   o619 b620 b3346
9901    H       h3352   z t3352
9902    S       s3352   t671 h h1778 h3258 h3259 h3352
9903    G       s3352   t3339
9904    B       b3352   s3352
9905    T       t3355   o695 b3352 b3252
9906    B       b3355   t3355
9907    B       b3356   t3227
9908    B       b3358   t3352
9909    T       t3361   o619 b3356 b3358
9910    H       h3361   v_2 t3361
9911    S       s3361   t671 h h1778 h3258 h3361
9912    G       s3361   t3339
9913    B       b3361   s3361
9914    T       t3364   o695 b3361 b3252
9915    B       b3364   t3364
9916    H       h3364   v_2 t3230
9917    S       s3364   t671 h h1778 h3258 h3364
9918    G       s3364   t3339
9919    B       b3365   s3364
9920    T       t3365   o695 b3365 b3252
9921    B       b3366   t3365
9922    S       s3366   t671 h h1780 h3258 h3364
9923    G       s3366   t3339
9924    B       b3367   s3366
9925    T       t3367   o695 b3367 b3252
9926    B       b3368   t3367
9927    S       s3368   t671 h h1780 h3258
9928    G       s3368   t3339
9929    B       b3369   s3368
9930    T       t3369   o695 b3369 b3252
9931    B       b3370   t3369
9932    S       s3370   t671 h h1780
9933    G       s3370   t3339
9934    B       b3371   s3370
9935    T       t3371   o695 b3371 b3252
9936    B       b3372   t3371
9937    T       t3372   o2 b3258
9938    B       b3373   t3372
9939    T       t3373   o694 b3372 b4 b3373
9940    B       b3374   t3373
9941    T       t3374   o2 b3374
9942    B       b3375   t3374
9943    T       t3375   o694 b3370 b4 b3375
9944    B       b3390   t3375
9945    T       t3399   o2 b3390
9946    B       b3439   t3399
9947    T       t3439   o694 b3368 b4 b3439
9948    B       b3440   t3439
9949    T       t3440   o2 b3440
9950    B       b3441   t3440
9951    T       t3441   o694 b3366 b4 b3441
9952    B       b3485   t3441
9953    T       t3485   o2 b3485
9954    B       b3486   t3485
9955    T       t3486   o694 b3364 b4 b3486
9956    B       b3487   t3486
9957    T       t3487   o2 b3487
9958    B       b3488   t3487
9959    T       t3488   o694 b3355 b4 b3488
9960    B       b3489   t3488
9961    T       t3489   o2 b3489
9962    B       b3490   t3489
9963    T       t3490   o694 b3321 b4 b3490
9964    B       b3491   t3490
9965    T       t3491   o2 b3491
9966    B       b3492   t3491
9967    T       t3492   o694 b3317 b4 b3492
9968    B       b3493   t3492
9969    T       t3493   o2 b3493
9970    B       b3495   t3493
9971    T       t3495   o694 b3313 b4 b3495
9972    B       b3496   t3495
9973    T       t3496   o2 b3496
9974    B       b3497   t3496
9975    T       t3497   o694 b3309 b4 b3497
9976    B       b3498   t3497
9977    T       t3498   o2 b3498
9978    B       b3499   t3498
9979    T       t3499   o694 b3305 b4 b3499
9980    B       b3500   t3499
9981    T       t3500   o2 b3500
9982    B       b3501   t3500
9983    T       t3501   o694 b3303 b4 b3501
9984    B       b3502   t3501
9985    T       t3502   o2 b3502
9986    B       b3503   t3502
9987    T       t3503   o694 b3301 b4 b3503
9988    B       b3504   t3503
9989    T       t3504   o2 b3504
9990    B       b3505   t3504
9991    T       t3505   o694 b3299 b4 b3505
9992    B       b3506   t3505
9993    T       t3506   o2 b3506
9994    B       b3507   t3506
9995    T       t3507   o694 b3297 b711 b3507
9996    B       b3508   t3507
9997    T       t3508   o2 b3508
9998    B       b3509   t3508
9999    T       t3509   o694 b3292 b711 b3509
10000    B       b3510   t3509
10001    T       t3510   o2 b3510
10002    B       b3511   t3510
10003    T       t3511   o694 b3290 b4 b3511
10004    B       b3512   t3511
10005    T       t3512   o b3512 b4
10006    B       b3513   t3512
10007    T       t3513   o693 b3258 b3513
10008    B       b3514   t3513
10009    P       p3514   String "setSubstT << equal{car{'h1}; inv_image{car{'g1}; x. 'f['x]; car{'h2}}} >> 16 ttca thenT dT 17 ttca thenT funSetT 18 ttca"
10010    O       o3514   ext_rule p3514
10011    T       t3514   o693 b3512 b4
10012    B       b3515   t3514
10013    T       t3515   o3514 b692 b3515 b4 b4
10014    B       b3516   t3515
10015    T       t3516   o b3516 b4
10016    B       b3517   t3516
10017    T       t3517   o3240 b692 b3514 b3517 b4
10018    B       b3518   t3517
10019    T       t3518   o690 b3518
10020    B       b3519   t3518
10021    T       t3519   o3227 b3331 b3240 b3519 b4
10022    B       b3520   t3519
10023    T       t6621   o6621 b3520
10024    B       b6621   t6621
10025    P       p6622   Number 8836
10026    P       p6623   Number 9143
10027    O       o6623   location p6622 p6623
10028    P       p3875   String kernel_type
10029    O       o3875   rule p3875
10030    T       t3875   o664 b665 b2993 b2993
10031    S       s3875   t664 h
10032    G       s3875   t3875
10033    B       b3876   s3875
10034    T       t3876   o662 b3876
10035    B       b3877   t3876
10036    T       t3877   o681 b2997
10037    S       s3877   t671 h
10038    G       s3877   t3877
10039    B       b3878   s3877
10040    T       t3878   o662 b3878
10041    B       b3880   t3878
10042    T       t3880   o661 b681 b3880
10043    B       b3881   t3880
10044    T       t3881   o661 b3877 b3881
10045    B       b3882   t3881
10046    T       t3882   o661 b669 b3882
10047    B       b3883   t3882
10048    T       t3883   o661 b667 b3883
10049    B       b3884   t3883
10050    P       p3884   String "rwh unfold_kernel 0 thenT autoT"
10051    O       o3884   ext_rule p3884
10052    T       t3884   o b3876 b695
10053    B       b3885   t3884
10054    T       t3885   o b668 b3885
10055    B       b3886   t3885
10056    T       t3886   o b666 b3886
10057    B       b3887   t3886
10058    T       t3887   o695 b3878 b3887
10059    B       b3888   t3887
10060    T       t3888   o694 b3888 b4 b703
10061    B       b3889   t3888
10062    T       t3889   o693 b3889 b4
10063    B       b3890   t3889
10064    T       t3890   o3884 b692 b3890 b4 b4
10065    B       b3891   t3890
10066    T       t3891   o690 b3891
10067    B       b3892   t3891
10068    P       p6624   Number 8863
10069    P       p6625   Number 8871
10070    O       o6625   resource_defs p6624 p6625 p264
10071    P       p6626   Number 8869
10072    O       o6626   uid p6626 p6625
10073    T       t6626   o6626 b784
10074    B       b6626   t6626
10075    T       t6627   o b6626 b4
10076    B       b6627   t6627
10077    T       t6628   o6625 b6627
10078    B       b6628   t6628
10079    T       t6629   o b6628 b4
10080    B       b6629   t6629
10081    T       t6630   o3875 b661 b3884 b3892 b6629
10082    B       b6630   t6630
10083    T       t6631   o6623 b6630
10084    B       b6631   t6631
10085    P       p6631   Number 9145
10086    P       p6632   Number 9567
10087    O       o6632   location p6631 p6632
10088    P       p3901   String kernel_intro
10089    O       o3901   rule p3901
10090    S       s3901   t671 h
10091    G       s3901   t3022
10092    B       b3901   s3901
10093    T       t3901   o662 b3901
10094    B       b3902   t3901
10095    S       s3902   t671 h
10096    G       s3902   t2997
10097    B       b3903   s3902
10098    T       t3903   o662 b3903
10099    B       b3904   t3903
10100    T       t3904   o661 b3902 b3904
10101    B       b3905   t3904
10102    T       t3905   o661 b2708 b3905
10103    B       b3906   t3905
10104    T       t3906   o661 b3877 b3906
10105    B       b3907   t3906
10106    T       t3907   o661 b669 b3907
10107    B       b3908   t3907
10108    T       t3908   o661 b667 b3908
10109    B       b3909   t3908
10110    T       t3909   o b3901 b4
10111    B       b3910   t3909
10112    T       t3910   o b2707 b3910
10113    B       b3911   t3910
10114    T       t3911   o b3876 b3911
10115    B       b3912   t3911
10116    T       t3912   o b668 b3912
10117    B       b3913   t3912
10118    T       t3913   o b666 b3913
10119    B       b3914   t3913
10120    T       t3914   o695 b3903 b3914
10121    B       b3915   t3914
10122    T       t3915   o694 b3915 b4 b703
10123    B       b3916   t3915
10124    T       t3916   o693 b3916 b4
10125    B       b3921   t3916
10126    T       t3921   o3884 b692 b3921 b4 b4
10127    B       b3922   t3921
10128    T       t3922   o690 b3922
10129    B       b3923   t3922
10130    P       p6633   Number 9173
10131    P       p6634   Number 9181
10132    O       o6634   resource_defs p6633 p6634 p264
10133    P       p6635   Number 9179
10134    O       o6635   uid p6635 p6634
10135    T       t6635   o6635 b784
10136    B       b6635   t6635
10137    T       t6636   o b6635 b4
10138    B       b6636   t6636
10139    T       t6637   o6634 b6636
10140    B       b6637   t6637
10141    T       t6638   o b6637 b4
10142    B       b6638   t6638
10143    T       t6639   o3901 b661 b3909 b3923 b6638
10144    B       b6639   t6639
10145    T       t6640   o6632 b6639
10146    B       b6640   t6640
10147    P       p6640   Number 9671
10148    P       p6641   Number 10032
10149    O       o6641   location p6640 p6641
10150    P       p3932   String kernel_subgroup
10151    O       o3932   rule p3932
10152    T       t3932   o1834 b2993
10153    B       b3932   t3932
10154    T       t3933   o b3932 b4
10155    B       b3933   t3933
10156    T       t3934   o b3190 b3933
10157    B       b3934   t3934
10158    T       t3935   o b660 b3934
10159    B       b3935   t3935
10160    T       t3936   o3339 b2993 b576
10161    S       s3936   t671 h
10162    G       s3936   t3936
10163    B       b3936   s3936
10164    T       t3937   o662 b3936
10165    B       b3937   t3937
10166    T       t3938   o661 b3339 b3937
10167    B       b3938   t3938
10168    T       t3939   o661 b3904 b3938
10169    B       b3939   t3939
10170    T       t3940   o661 b3877 b3939
10171    B       b3940   t3940
10172    T       t3941   o661 b669 b3940
10173    B       b3941   t3941
10174    T       t3942   o661 b667 b3941
10175    B       b3942   t3942
10176    P       p3942   String "assumT 4 thenT rwh unfold_kernel 2 thenT rwh unfold_group_bvd 2 thenT rwh unfold_hom 2 thenT autoT"
10177    O       o3942   ext_rule p3942
10178    T       t3943   o b3338 b4
10179    B       b3943   t3943
10180    T       t3944   o b3903 b3943
10181    B       b3944   t3944
10182    T       t3945   o b3876 b3944
10183    B       b3945   t3945
10184    T       t3946   o b668 b3945
10185    B       b3946   t3946
10186    T       t3947   o b666 b3946
10187    B       b3947   t3947
10188    T       t3948   o695 b3936 b3947
10189    B       b3948   t3948
10190    T       t3949   o694 b3948 b4 b703
10191    B       b3949   t3949
10192    H       h3949   y_7 t620
10193    H       h3950   y t621
10194    T       t3950   o620 b2993
10195    H       h3951   y_1 t3950
10196    H       h3952   y_2 t620
10197    T       t3952   o621 b3022
10198    H       h3953   y_3 t3952
10199    T       t3953   o624 b2993
10200    B       b3953   t3953
10201    T       t3954   o952 b3953 b3022
10202    H       h3954   y_4 t3954
10203    T       t3955   o629 b630 b3953
10204    B       b3955   t3955
10205    T       t3956   o629 b636 b3953
10206    B       b3956   t3956
10207    T       t3957   o532 b2993
10208    B       b3957   t3957
10209    T       t3958   o637 b2993 b630 b636
10210    B       b3958   t3958
10211    T       t3959   o623 b3953 b3957 b3958 b638
10212    B       b3959   t3959
10213    T       t3960   o635 b3956 b3959
10214    B       b3960   t3960
10215    T       t3961   o635 b3955 b3960
10216    B       b3961   t3961 b
10217    T       t3962   o633 b634 b3961
10218    B       b3962   t3962 a
10219    T       t3963   o633 b634 b3962
10220    H       h3963   y_5 t3963
10221    T       t3964   o623 b3953 b3957 b630 b636
10222    B       b3964   t3964
10223    T       t3965   o635 b3964 b3875
10224    B       b3965   t3965 b
10225    T       t3966   o633 b634 b3965
10226    B       b3966   t3966 a
10227    T       t3967   o633 b634 b3966
10228    H       h3967   y_6 t3967
10229    T       t3968   o635 b3875 b3964
10230    B       b3968   t3968
10231    T       t3969   o635 b3956 b3968
10232    B       b3969   t3969
10233    T       t3970   o635 b3955 b3969
10234    B       b3970   t3970 b
10235    T       t3971   o633 b634 b3970
10236    B       b3971   t3971 a
10237    T       t3972   o633 b634 b3971
10238    H       h3972   z t3972
10239    T       t3973   o629 b581 b3953
10240    H       h3973   y t3973
10241    S       s3973   t671 h h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10242    G       s3973   t797
10243    B       b3973   s3973
10244    T       t3974   o695 b3973 b3947
10245    B       b3974   t3974
10246    T       t3975   o3397 b3953 b624
10247    S       s3975   t671 h h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10248    G       s3975   t3975
10249    B       b3975   s3975
10250    T       t3976   o695 b3975 b3947
10251    B       b3976   t3976
10252    S       s3976   t671 h h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10253    G       s3976   t3936
10254    B       b3977   s3976
10255    T       t3977   o695 b3977 b3947
10256    B       b3978   t3977
10257    S       s3978   t671 h h3949 h3950 h3718 h1274 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10258    G       s3978   t3936
10259    B       b3979   s3978
10260    T       t3979   o695 b3979 b3947
10261    B       b3980   t3979
10262    S       s3980   t671 h h3949 h3950 h1276 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10263    G       s3980   t3936
10264    B       b3981   s3980
10265    T       t3981   o695 b3981 b3947
10266    B       b3982   t3981
10267    S       s3982   t671 h h3949 h1278 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10268    G       s3982   t3936
10269    B       b3983   s3982
10270    T       t3983   o695 b3983 b3947
10271    B       b3984   t3983
10272    H       h3984   y t309
10273    S       s3984   t671 h h3984 h3951 h3952 h3953 h3954 h3963 h3967 h3972
10274    G       s3984   t3936
10275    B       b3985   s3984
10276    T       t3985   o695 b3985 b3947
10277    B       b3986   t3985
10278    B       b3987   t3967
10279    B       b3988   t3972
10280    T       t3988   o619 b3987 b3988
10281    H       h3988   z_1 t3988
10282    S       s3988   t671 h h3984 h3951 h3952 h3953 h3954 h3963 h3988
10283    G       s3988   t3936
10284    B       b3989   s3988
10285    T       t3989   o695 b3989 b3947
10286    B       b3990   t3989
10287    B       b3991   t3963
10288    B       b3992   t3988
10289    T       t3992   o619 b3991 b3992
10290    H       h3992   z t3992
10291    S       s3992   t671 h h3984 h3951 h3952 h3953 h3954 h3992
10292    G       s3992   t3936
10293    B       b3993   s3992
10294    T       t3993   o695 b3993 b3947
10295    B       b3994   t3993
10296    B       b3995   t3954
10297    B       b3996   t3992
10298    T       t3996   o619 b3995 b3996
10299    H       h3996   z_1 t3996
10300    S       s3996   t671 h h3984 h3951 h3952 h3953 h3996
10301    G       s3996   t3936
10302    B       b3997   s3996
10303    T       t3997   o695 b3997 b3947
10304    B       b3998   t3997
10305    B       b3999   t3952
10306    B       b4000   t3996
10307    T       t4000   o619 b3999 b4000
10308    H       h4000   z t4000
10309    S       s4000   t671 h h3984 h3951 h3952 h4000
10310    G       s4000   t3936
10311    B       b4001   s4000
10312    T       t4001   o695 b4001 b3947
10313    B       b4002   t4001
10314    B       b4003   t4000
10315    T       t4003   o619 b620 b4003
10316    H       h4003   z_1 t4003
10317    S       s4003   t671 h h3984 h3951 h4003
10318    G       s4003   t3936
10319    B       b4004   s4003
10320    T       t4004   o695 b4004 b3947
10321    B       b4005   t4004
10322    B       b4006   t3950
10323    B       b4007   t4003
10324    T       t4007   o619 b4006 b4007
10325    H       h4007   z t4007
10326    S       s4007   t671 h h3984 h4007
10327    G       s4007   t3936
10328    B       b4008   s4007
10329    T       t4008   o695 b4008 b3947
10330    B       b4009   t4008
10331    B       b4010   t4007
10332    T       t4010   o619 b309 b4010
10333    H       h4010   v t4010
10334    S       s4010   t671 h h4010
10335    G       s4010   t3936
10336    B       b4011   s4010
10337    T       t4011   o695 b4011 b3947
10338    B       b4012   t4011
10339    T       t4012   o619 b480 b4010
10340    H       h4012   v t4012
10341    S       s4012   t671 h h4012
10342    G       s4012   t3936
10343    B       b4013   s4012
10344    T       t4013   o695 b4013 b3947
10345    B       b4014   t4013
10346    H       h4014   v t3026
10347    S       s4014   t671 h h4014
10348    G       s4014   t3936
10349    B       b4015   s4014
10350    T       t4015   o695 b4015 b3947
10351    B       b4016   t4015
10352    H       h4016   v t2997
10353    S       s4016   t671 h h4016
10354    G       s4016   t3936
10355    B       b4017   s4016
10356    T       t4017   o695 b4017 b3947
10357    B       b4018   t4017
10358    T       t4018   o2 b3949
10359    B       b4019   t4018
10360    T       t4019   o694 b4018 b4 b4019
10361    B       b4020   t4019
10362    T       t4020   o2 b4020
10363    B       b4021   t4020
10364    T       t4021   o694 b4016 b4 b4021
10365    B       b4022   t4021
10366    T       t4022   o2 b4022
10367    B       b4023   t4022
10368    T       t4023   o694 b4014 b4 b4023
10369    B       b4024   t4023
10370    T       t4024   o2 b4024
10371    B       b4025   t4024
10372    T       t4025   o694 b4012 b4 b4025
10373    B       b4026   t4025
10374    T       t4026   o2 b4026
10375    B       b4027   t4026
10376    T       t4027   o694 b4009 b4 b4027
10377    B       b4028   t4027
10378    T       t4028   o2 b4028
10379    B       b4029   t4028
10380    T       t4029   o694 b4005 b4 b4029
10381    B       b4030   t4029
10382    T       t4030   o2 b4030
10383    B       b4031   t4030
10384    T       t4031   o694 b4002 b4 b4031
10385    B       b4032   t4031
10386    T       t4032   o2 b4032
10387    B       b4033   t4032
10388    T       t4033   o694 b3998 b4 b4033
10389    B       b4034   t4033
10390    T       t4034   o2 b4034
10391    B       b4035   t4034
10392    T       t4035   o694 b3994 b4 b4035
10393    B       b4036   t4035
10394    T       t4036   o2 b4036
10395    B       b4037   t4036
10396    T       t4037   o694 b3990 b4 b4037
10397    B       b4038   t4037
10398    T       t4038   o2 b4038
10399    B       b4039   t4038
10400    T       t4039   o694 b3986 b4 b4039
10401    B       b4040   t4039
10402    T       t4040   o2 b4040
10403    B       b4041   t4040
10404    T       t4041   o694 b3984 b4 b4041
10405    B       b4042   t4041
10406    T       t4042   o2 b4042
10407    B       b4043   t4042
10408    T       t4043   o694 b3982 b4 b4043
10409    B       b4044   t4043
10410    T       t4044   o2 b4044
10411    B       b4045   t4044
10412    T       t4045   o694 b3980 b4 b4045
10413    B       b4046   t4045
10414    T       t4046   o2 b4046
10415    B       b4047   t4046
10416    T       t4047   o694 b3978 b711 b4047
10417    B       b4048   t4047
10418    T       t4048   o2 b4048
10419    B       b4049   t4048
10420    T       t4049   o694 b3976 b711 b4049
10421    B       b4050   t4049
10422    T       t4050   o2 b4050
10423    B       b4051   t4050
10424    T       t4051   o694 b3974 b4 b4051
10425    B       b4052   t4051
10426    T       t4052   o b4052 b4
10427    B       b4053   t4052
10428    T       t4053   o693 b3949 b4053
10429    B       b4054   t4053
10430    P       p4054   String "setSubstT << equal{car{'h}; setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; id{'g2}}}} >> 15 ttca thenT dT 16 thenT autoT thenT funSetT 17 ttca"
10431    O       o4054   ext_rule p4054
10432    H       h4054   y_8 t621
10433    H       h4055   y_9 t530
10434    H       h4056   y_10 t269
10435    S       s4056   t671 h h3949 h4054 h4055 h4056 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10436    G       s4056   t797
10437    B       b4056   s4056
10438    T       t4056   o695 b4056 b3947
10439    B       b4057   t4056
10440    S       s4057   t671 h h3949 h4054 h4055 h1274 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10441    G       s4057   t797
10442    B       b4058   s4057
10443    T       t4058   o695 b4058 b3947
10444    B       b4059   t4058
10445    S       s4059   t671 h h3949 h4054 h1276 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10446    G       s4059   t797
10447    B       b4060   s4059
10448    T       t4060   o695 b4060 b3947
10449    B       b4061   t4060
10450    S       s4061   t671 h h3949 h1278 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10451    G       s4061   t797
10452    B       b4062   s4061
10453    T       t4062   o695 b4062 b3947
10454    B       b4063   t4062
10455    S       s4063   t671 h h3984 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h678 h3973
10456    G       s4063   t797
10457    B       b4064   s4063
10458    T       t4064   o695 b4064 b3947
10459    B       b4065   t4064
10460    S       s4065   t671 h h3984 h3951 h3952 h3953 h3954 h3963 h3988 h678 h3973
10461    G       s4065   t797
10462    B       b4066   s4065
10463    T       t4066   o695 b4066 b3947
10464    B       b4067   t4066
10465    S       s4067   t671 h h3984 h3951 h3952 h3953 h3954 h3992 h678 h3973
10466    G       s4067   t797
10467    B       b4068   s4067
10468    T       t4068   o695 b4068 b3947
10469    B       b4069   t4068
10470    S       s4069   t671 h h3984 h3951 h3952 h3953 h3996 h678 h3973
10471    G       s4069   t797
10472    B       b4070   s4069
10473    T       t4070   o695 b4070 b3947
10474    B       b4071   t4070
10475    S       s4071   t671 h h3984 h3951 h3952 h4000 h678 h3973
10476    G       s4071   t797
10477    B       b4072   s4071
10478    T       t4072   o695 b4072 b3947
10479    B       b4073   t4072
10480    S       s4073   t671 h h3984 h3951 h4003 h678 h3973
10481    G       s4073   t797
10482    B       b4074   s4073
10483    T       t4074   o695 b4074 b3947
10484    B       b4075   t4074
10485    S       s4075   t671 h h3984 h4007 h678 h3973
10486    G       s4075   t797
10487    B       b4076   s4075
10488    T       t4076   o695 b4076 b3947
10489    B       b4077   t4076
10490    H       h4077   y t480
10491    S       s4077   t671 h h4077 h4007 h678 h3973
10492    G       s4077   t797
10493    B       b4078   s4077
10494    T       t4078   o695 b4078 b3947
10495    B       b4079   t4078
10496    H       h4079   z t3022
10497    S       s4079   t671 h h4077 h4079 h678 h3973
10498    G       s4079   t797
10499    B       b4080   s4079
10500    T       t4080   o695 b4080 b3947
10501    B       b4081   t4080
10502    S       s4081   t671 h h4077 h4079
10503    G       s4081   t3975
10504    B       b4082   s4081
10505    T       t4082   o695 b4082 b3947
10506    B       b4083   t4082
10507    S       s4083   t671 h h4077 h4079
10508    G       s4083   t3936
10509    B       b4084   s4083
10510    T       t4084   o695 b4084 b3947
10511    B       b4085   t4084
10512    T       t4085   o694 b4085 b711 b4023
10513    B       b4086   t4085
10514    T       t4086   o2 b4086
10515    B       b4087   t4086
10516    T       t4087   o694 b4083 b711 b4087
10517    B       b4088   t4087
10518    T       t4088   o2 b4088
10519    B       b4096   t4088
10520    T       t4106   o694 b4081 b4 b4096
10521    B       b4106   t4106
10522    T       t4122   o2 b4106
10523    B       b4123   t4122
10524    T       t4141   o694 b4079 b4 b4123
10525    B       b4147   t4141
10526    T       t4147   o2 b4147
10527    B       b4155   t4147
10528    T       t4155   o694 b4077 b4 b4155
10529    B       b4157   t4155
10530    T       t4164   o2 b4157
10531    B       b4165   t4164
10532    T       t4165   o694 b4075 b4 b4165
10533    B       b4167   t4165
10534    T       t4167   o2 b4167
10535    B       b4169   t4167
10536    T       t4173   o694 b4073 b4 b4169
10537    B       b4174   t4173
10538    T       t4174   o2 b4174
10539    B       b4175   t4174
10540    T       t4175   o694 b4071 b4 b4175
10541    B       b4176   t4175
10542    T       t4176   o2 b4176
10543    B       b4177   t4176
10544    T       t4177   o694 b4069 b4 b4177
10545    B       b4178   t4177
10546    T       t4178   o2 b4178
10547    B       b4179   t4178
10548    T       t4179   o694 b4067 b4 b4179
10549    B       b4180   t4179
10550    T       t4180   o2 b4180
10551    B       b4181   t4180
10552    T       t4181   o694 b4065 b4 b4181
10553    B       b4182   t4181
10554    T       t4182   o2 b4182
10555    B       b4183   t4182
10556    T       t4183   o694 b4063 b4 b4183
10557    B       b4184   t4183
10558    T       t4184   o2 b4184
10559    B       b4185   t4184
10560    T       t4185   o694 b4061 b4 b4185
10561    B       b4186   t4185
10562    T       t4186   o2 b4186
10563    B       b4187   t4186
10564    T       t4187   o694 b4059 b4 b4187
10565    B       b4188   t4187
10566    T       t4188   o2 b4188
10567    B       b4189   t4188
10568    T       t4189   o694 b4057 b4 b4189
10569    B       b4190   t4189
10570    T       t4190   o693 b4190 b4
10571    B       b4191   t4190
10572    T       t4192   o4054 b692 b4191 b4 b4
10573    B       b4193   t4192
10574    T       t4205   o b4193 b4
10575    B       b4206   t4205
10576    T       t4206   o3942 b692 b4054 b4206 b4
10577    B       b4207   t4206
10578    T       t4207   o690 b4207
10579    B       b4208   t4207
10580    T       t4208   o3932 b3935 b3942 b4208 b4
10581    B       b4209   t4208
10582    T       t6641   o6641 b4209
10583    B       b6641   t6641
10584    P       p6642   Number 10034
10585    P       p6643   Number 10643
10586    O       o6643   location p6642 p6643
10587    P       p3544   String kernel_subgroup_elim
10588    O       o3544   rule p3544
10589    H       h3544   u t2997
10590    S       s3544   t664 h h3544 h1115
10591    G       s3544   t666
10592    B       b3544   s3544
10593    T       t3544   o662 b3544
10594    B       b3545   t3544
10595    S       s3545   t664 h h3544 h1115
10596    G       s3545   t668
10597    B       b3546   s3545
10598    T       t3546   o662 b3546
10599    B       b3547   t3546
10600    S       s3547   t664 h h3544 h1115
10601    G       s3547   t3875
10602    B       b3548   s3547
10603    T       t3548   o662 b3548
10604    B       b3549   t3548
10605    S       s3549   t671 h h3544 h1115
10606    G       s3549   t628
10607    B       b3550   s3549
10608    T       t3550   o662 b3550
10609    B       b3551   t3550
10610    H       h3551   v t3936
10611    S       s3551   t671 h h3544 h1115 h3551
10612    G       s3551   t2050
10613    B       b3552   s3551
10614    T       t3552   o662 b3552
10615    B       b3553   t3552
10616    S       s3553   t671 h h3544 h1115
10617    G       s3553   t2050
10618    B       b3554   s3553
10619    T       t3554   o662 b3554
10620    B       b3555   t3554
10621    T       t3555   o661 b3553 b3555
10622    B       b3556   t3555
10623    T       t3556   o661 b3551 b3556
10624    B       b3557   t3556
10625    T       t3557   o661 b3549 b3557
10626    B       b3558   t3557
10627    T       t3558   o661 b3547 b3558
10628    B       b3559   t3558
10629    T       t3559   o661 b3545 b3559
10630    B       b3560   t3559
10631    P       p3560   String "assertT << subgroup{'h; 'g1} >> ttca"
10632    O       o3560   ext_rule p3560
10633    T       t3560   o b3552 b4
10634    B       b3561   t3560
10635    T       t3561   o b3550 b3561
10636    B       b3562   t3561
10637    T       t3562   o b3548 b3562
10638    B       b3563   t3562
10639    T       t3563   o b3546 b3563
10640    B       b3564   t3563
10641    T       t3564   o b3544 b3564
10642    B       b3565   t3564
10643    T       t3565   o695 b3554 b3565
10644    B       b3566   t3565
10645    T       t3566   o694 b3566 b4 b703
10646    B       b3567   t3566
10647    S       s3567   t671 h h3544 h1115
10648    G       s3567   t3936
10649    B       b3568   s3567
10650    T       t3568   o695 b3568 b3565
10651    B       b3569   t3568
10652    T       t3569   o2 b3567
10653    B       b3570   t3569
10654    T       t3570   o2266 b3569 b4 b3570
10655    B       b3571   t3570
10656    T       t3571   o b3571 b4
10657    B       b3572   t3571
10658    T       t3572   o693 b3567 b3572
10659    B       b3573   t3572
10660    P       p3573   String "copyHypT 2 2 thenT rwh unfold_kernel 3 thenT rwh unfold_group_bvd 3 thenT rwh unfold_hom 3 thenT autoT"
10661    O       o3573   ext_rule p3573
10662    S       s3573   t671 h h3544 h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115 h678 h3973
10663    G       s3573   t797
10664    B       b3574   s3573
10665    T       t3574   o695 b3574 b3565
10666    B       b3575   t3574
10667    S       s3575   t671 h h3544 h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10668    G       s3575   t3975
10669    B       b3576   s3575
10670    T       t3576   o695 b3576 b3565
10671    B       b3577   t3576
10672    S       s3577   t671 h h3544 h3949 h3950 h3718 h3719 h941 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10673    G       s3577   t3936
10674    B       b3578   s3577
10675    T       t3578   o695 b3578 b3565
10676    B       b3579   t3578
10677    S       s3579   t671 h h3544 h3949 h3950 h3718 h1274 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10678    G       s3579   t3936
10679    B       b3580   s3579
10680    T       t3580   o695 b3580 b3565
10681    B       b3581   t3580
10682    S       s3581   t671 h h3544 h3949 h3950 h1276 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10683    G       s3581   t3936
10684    B       b3582   s3581
10685    T       t3582   o695 b3582 b3565
10686    B       b3583   t3582
10687    S       s3583   t671 h h3544 h3949 h1278 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10688    G       s3583   t3936
10689    B       b3584   s3583
10690    T       t3584   o695 b3584 b3565
10691    B       b3585   t3584
10692    S       s3585   t671 h h3544 h3984 h3951 h3952 h3953 h3954 h3963 h3967 h3972 h1115
10693    G       s3585   t3936
10694    B       b3586   s3585
10695    T       t3586   o695 b3586 b3565
10696    B       b3587   t3586
10697    S       s3587   t671 h h3544 h3984 h3951 h3952 h3953 h3954 h3963 h3988 h1115
10698    G       s3587   t3936
10699    B       b3588   s3587
10700    T       t3588   o695 b3588 b3565
10701    B       b3589   t3588
10702    S       s3589   t671 h h3544 h3984 h3951 h3952 h3953 h3954 h3992 h1115
10703    G       s3589   t3936
10704    B       b3590   s3589
10705    T       t3590   o695 b3590 b3565
10706    B       b3591   t3590
10707    S       s3591   t671 h h3544 h3984 h3951 h3952 h3953 h3996 h1115
10708    G       s3591   t3936
10709    B       b3592   s3591
10710    T       t3592   o695 b3592 b3565
10711    B       b3593   t3592
10712    S       s3593   t671 h h3544 h3984 h3951 h3952 h4000 h1115
10713    G       s3593   t3936
10714    B       b3594   s3593
10715    T       t3594   o695 b3594 b3565
10716    B       b3595   t3594
10717    S       s3595   t671 h h3544 h3984 h3951 h4003 h1115
10718    G       s3595   t3936
10719    B       b3596   s3595