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

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

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

revision 3566 by xiny, Sun Mar 24 08:21:13 2002 UTC revision 3567 by xiny, Tue Apr 9 05:57:26 2002 UTC
# Line 965  Line 965 
965  T       t358    o1 b357  T       t358    o1 b357
966  B       b358    t358  B       b358    t358
967  P       p358    Number 20  P       p358    Number 20
968  P       p359    Number 42  P       p6      Number 43
969  O       o359    location p358 p359  O       o8      location p358 p6
970    P       p8      String Czf_itt_set_bvd
971    O       o10     parent p8
972    T       t215    o10
973    B       b215    t215
974    T       t218    o b215 b4
975    B       b218    t218
976    P       p226    String Czf_itt_dexists
977    O       o226    parent p226
978    T       t230    o226
979    B       b230    t230
980    T       t233    o b230 b4
981    B       b233    t233
982    P       p249    String Czf_itt_dall
983    O       o249    parent p249
984    T       t269    o249
985    B       b269    t269
986    T       t270    o b269 b4
987    B       b270    t270
988    P       p283    String Czf_itt_set_ind
989    O       o283    parent p283
990    T       t309    o283
991    B       b309    t309
992    T       t310    o b309 b4
993    B       b310    t310
994    P       p323    String Czf_itt_all
995    O       o323    parent p323
996    T       t368    o323
997    B       b369    t368
998    T       t369    o b369 b4
999    B       b370    t369
1000    P       p373    String Czf_itt_sep
1001    O       o374    parent p373
1002    T       t508    o374
1003    B       b508    t508
1004    T       t509    o b508 b4
1005    B       b509    t509
1006  P       p360    String Czf_itt_member  P       p360    String Czf_itt_member
1007  O       o360    parent p360  O       o360    parent p360
1008  T       t360    o360  T       t360    o360
# Line 983  Line 1019 
1019  B       b364    t364  B       b364    t364
1020  T       t365    o b361 b364  T       t365    o b361 b364
1021  B       b365    t365  B       b365    t365
1022  T       t366    o2 b361 b365 b356  T       t515    o b509 b365
1023  B       b366    t366  B       b515    t515
1024  T       t367    o359 b366  T       t516    o b370 b515
1025  B       b367    t367  B       b516    t516
1026  P       p367    Number 44  T       t522    o b310 b516
1027  P       p368    Number 55  B       b522    t522
1028  O       o368    location p367 p368  T       t523    o b270 b522
1029    B       b523    t523
1030    T       t524    o b233 b523
1031    B       b524    t524
1032    T       t526    o b218 b524
1033    B       b526    t526
1034    T       t532    o2 b218 b526 b356
1035    B       b532    t532
1036    T       t533    o8 b532
1037    B       b533    t533
1038    P       p533    Number 45
1039  NSummary!summary_item   summary_item    summary_item Summary  NSummary!summary_item   summary_item    summary_item Summary
1040  O       o369    summary_item  O       o369    summary_item
1041  NOcaml!str_open str_open        str_open Ocaml  NOcaml!str_open str_open        str_open Ocaml
 O       o370    str_open p367 p368  
1042  NOcaml!string   string  string Ocaml  NOcaml!string   string  string Ocaml
1043  P       p370    String Printf  P       p370    String Printf
1044  O       o371    string p370  O       o371    string p370
# Line 1001  Line 1046 
1046  B       b371    t371  B       b371    t371
1047  T       t372    o b371 b4  T       t372    o b371 b4
1048  B       b372    t372  B       b372    t372
 T       t373    o370 b372  
 B       b373    t373  
 T       t374    o369 b373  
 B       b374    t374  
 T       t375    o368 b374  
 B       b375    t375  
1049  P       p375    Number 56  P       p375    Number 56
1050  P       p376    Number 69  O       o533    location p533 p375
1051  O       o376    location p375 p376  O       o537    str_open p533 p375
1052  O       o377    str_open p375 p376  T       t569    o537 b372
1053    B       b570    t569
1054    T       t570    o369 b570
1055    B       b571    t570
1056    T       t571    o533 b571
1057    B       b572    t571
1058    P       p574    Number 57
1059  P       p377    String Mp_debug  P       p377    String Mp_debug
1060  O       o378    string p377  O       o378    string p377
1061  T       t378    o378  T       t378    o378
1062  B       b378    t378  B       b378    t378
1063  T       t379    o b378 b4  T       t379    o b378 b4
1064  B       b379    t379  B       b379    t379
 T       t380    o377 b379  
 B       b380    t380  
 T       t381    o369 b380  
 B       b381    t381  
 T       t382    o376 b381  
 B       b382    t382  
1065  P       p382    Number 70  P       p382    Number 70
1066  P       p383    Number 99  O       o578    location p574 p382
1067  O       o383    location p382 p383  O       o579    str_open p574 p382
1068  O       o384    str_open p382 p383  T       t593    o579 b379
1069    B       b593    t593
1070    T       t594    o369 b593
1071    B       b594    t594
1072    T       t596    o578 b594
1073    B       b596    t596
1074    P       p596    Number 71
1075  P       p384    String Refiner  P       p384    String Refiner
1076  O       o385    string p384  O       o385    string p384
1077  T       t385    o385  T       t385    o385
# Line 1041  Line 1086 
1086  B       b388    t388  B       b388    t388
1087  T       t389    o b385 b388  T       t389    o b385 b388
1088  B       b389    t389  B       b389    t389
 T       t390    o384 b389  
 B       b390    t390  
 T       t391    o369 b390  
 B       b391    t391  
 T       t392    o383 b391  
 B       b392    t392  
1089  P       p392    Number 100  P       p392    Number 100
1090  P       p393    Number 125  O       o596    location p596 p392
1091  O       o393    location p392 p393  O       o597    str_open p596 p392
1092  O       o394    str_open p392 p393  T       t597    o597 b389
1093    B       b597    t597
1094    T       t598    o369 b597
1095    B       b598    t598
1096    T       t599    o596 b598
1097    B       b599    t599
1098    P       p599    Number 101
1099  P       p394    String Term  P       p394    String Term
1100  O       o395    string p394  O       o395    string p394
1101  T       t395    o395  T       t395    o395
# Line 1061  Line 1106 
1106  B       b397    t397  B       b397    t397
1107  T       t398    o b385 b397  T       t398    o b385 b397
1108  B       b398    t398  B       b398    t398
 T       t399    o394 b398  
 B       b399    t399  
 T       t400    o369 b399  
 B       b400    t400  
 T       t401    o393 b400  
 B       b401    t401  
1109  P       p401    Number 126  P       p401    Number 126
1110  P       p402    Number 153  O       o599    location p599 p401
1111  O       o402    location p401 p402  O       o600    str_open p599 p401
1112  O       o403    str_open p401 p402  T       t600    o600 b398
1113    B       b600    t600
1114    T       t601    o369 b600
1115    B       b601    t601
1116    T       t602    o599 b601
1117    B       b602    t602
1118    P       p602    Number 127
1119  P       p403    String TermOp  P       p403    String TermOp
1120  O       o404    string p403  O       o404    string p403
1121  T       t404    o404  T       t404    o404
# Line 1081  Line 1126 
1126  B       b406    t406  B       b406    t406
1127  T       t407    o b385 b406  T       t407    o b385 b406
1128  B       b407    t407  B       b407    t407
 T       t408    o403 b407  
 B       b408    t408  
 T       t409    o369 b408  
 B       b409    t409  
 T       t410    o402 b409  
 B       b410    t410  
1129  P       p410    Number 154  P       p410    Number 154
1130  P       p411    Number 183  O       o602    location p602 p410
1131  O       o411    location p410 p411  O       o605    str_open p602 p410
1132  O       o412    str_open p410 p411  T       t623    o605 b407
1133    B       b623    t623
1134    T       t624    o369 b623
1135    B       b624    t624
1136    T       t625    o602 b624
1137    B       b625    t625
1138    P       p625    Number 155
1139  P       p412    String TermAddr  P       p412    String TermAddr
1140  O       o413    string p412  O       o413    string p412
1141  T       t413    o413  T       t413    o413
# Line 1101  Line 1146 
1146  B       b415    t415  B       b415    t415
1147  T       t416    o b385 b415  T       t416    o b385 b415
1148  B       b416    t416  B       b416    t416
 T       t417    o412 b416  
 B       b417    t417  
 T       t418    o369 b417  
 B       b418    t418  
 T       t419    o411 b418  
 B       b419    t419  
1149  P       p419    Number 184  P       p419    Number 184
1150  P       p420    Number 212  O       o625    location p625 p419
1151  O       o420    location p419 p420  O       o626    str_open p625 p419
1152  O       o421    str_open p419 p420  T       t626    o626 b416
1153    B       b626    t626
1154    T       t627    o369 b626
1155    B       b627    t627
1156    T       t628    o625 b627
1157    B       b628    t628
1158    P       p628    Number 185
1159  P       p421    String TermMan  P       p421    String TermMan
1160  O       o422    string p421  O       o422    string p421
1161  T       t422    o422  T       t422    o422
# Line 1121  Line 1166 
1166  B       b424    t424  B       b424    t424
1167  T       t425    o b385 b424  T       t425    o b385 b424
1168  B       b425    t425  B       b425    t425
 T       t426    o421 b425  
 B       b426    t426  
 T       t427    o369 b426  
 B       b427    t427  
 T       t428    o420 b427  
 B       b428    t428  
1169  P       p428    Number 213  P       p428    Number 213
1170  P       p429    Number 243  O       o628    location p628 p428
1171  O       o429    location p428 p429  O       o629    str_open p628 p428
1172  O       o430    str_open p428 p429  T       t629    o629 b425
1173    B       b629    t629
1174    T       t630    o369 b629
1175    B       b630    t630
1176    T       t631    o628 b630
1177    B       b631    t631
1178    P       p633    Number 214
1179  P       p430    String TermSubst  P       p430    String TermSubst
1180  O       o431    string p430  O       o431    string p430
1181  T       t431    o431  T       t431    o431
# Line 1141  Line 1186 
1186  B       b433    t433  B       b433    t433
1187  T       t434    o b385 b433  T       t434    o b385 b433
1188  B       b434    t434  B       b434    t434
 T       t435    o430 b434  
 B       b435    t435  
 T       t436    o369 b435  
 B       b436    t436  
 T       t437    o429 b436  
 B       b437    t437  
1189  P       p437    Number 244  P       p437    Number 244
1190  P       p438    Number 271  O       o633    location p633 p437
1191  O       o438    location p437 p438  O       o634    str_open p633 p437
1192  O       o439    str_open p437 p438  T       t636    o634 b434
1193    B       b647    t636
1194    T       t647    o369 b647
1195    B       b648    t647
1196    T       t649    o633 b648
1197    B       b649    t649
1198    P       p649    Number 245
1199  P       p439    String Refine  P       p439    String Refine
1200  O       o440    string p439  O       o440    string p439
1201  T       t440    o440  T       t440    o440
# Line 1161  Line 1206 
1206  B       b442    t442  B       b442    t442
1207  T       t443    o b385 b442  T       t443    o b385 b442
1208  B       b443    t443  B       b443    t443
 T       t444    o439 b443  
 B       b444    t444  
 T       t445    o369 b444  
 B       b445    t445  
 T       t446    o438 b445  
 B       b446    t446  
1209  P       p446    Number 272  P       p446    Number 272
1210  P       p447    Number 304  O       o649    location p649 p446
1211  O       o447    location p446 p447  O       o650    str_open p649 p446
1212  O       o448    str_open p446 p447  T       t650    o650 b443
1213    B       b650    t650
1214    T       t652    o369 b650
1215    B       b653    t652
1216    T       t653    o649 b653
1217    B       b654    t653
1218    P       p654    Number 273
1219  P       p448    String RefineError  P       p448    String RefineError
1220  O       o449    string p448  O       o449    string p448
1221  T       t449    o449  T       t449    o449
# Line 1181  Line 1226 
1226  B       b451    t451  B       b451    t451
1227  T       t452    o b385 b451  T       t452    o b385 b451
1228  B       b452    t452  B       b452    t452
 T       t453    o448 b452  
 B       b453    t453  
 T       t454    o369 b453  
 B       b454    t454  
 T       t455    o447 b454  
 B       b455    t455  
1229  P       p455    Number 305  P       p455    Number 305
1230  P       p456    Number 321  O       o654    location p654 p455
1231  O       o456    location p455 p456  O       o655    str_open p654 p455
1232  O       o457    str_open p455 p456  T       t655    o655 b452
1233    B       b655    t655
1234    T       t656    o369 b655
1235    B       b656    t656
1236    T       t657    o654 b656
1237    B       b657    t657
1238    P       p657    Number 306
1239    P       p658    Number 322
1240    O       o658    location p657 p658
1241    O       o659    str_open p657 p658
1242  P       p457    String Mp_resource  P       p457    String Mp_resource
1243  O       o458    string p457  O       o458    string p457
1244  T       t458    o458  T       t458    o458
1245  B       b458    t458  B       b458    t458
1246  T       t459    o b458 b4  T       t459    o b458 b4
1247  B       b459    t459  B       b459    t459
1248  T       t460    o457 b459  T       t659    o659 b459
1249  B       b460    t460  B       b659    t659
1250  T       t461    o369 b460  T       t660    o369 b659
1251  B       b461    t461  B       b660    t660
1252  T       t462    o456 b461  T       t661    o658 b660
1253  B       b462    t462  B       b661    t661
1254  P       p462    Number 323  P       p661    Number 324
 P       p463    Number 339  
 O       o463    location p462 p463  
 O       o464    str_open p462 p463  
1255  P       p464    String Tactic_type  P       p464    String Tactic_type
1256  O       o465    string p464  O       o465    string p464
1257  T       t465    o465  T       t465    o465
1258  B       b465    t465  B       b465    t465
1259  T       t466    o b465 b4  T       t466    o b465 b4
1260  B       b466    t466  B       b466    t466
 T       t467    o464 b466  
 B       b467    t467  
 T       t468    o369 b467  
 B       b468    t468  
 T       t469    o463 b468  
 B       b469    t469  
1261  P       p469    Number 340  P       p469    Number 340
1262  P       p470    Number 366  O       o661    location p661 p469
1263  O       o470    location p469 p470  O       o662    str_open p661 p469
1264  O       o471    str_open p469 p470  T       t662    o662 b466
1265    B       b662    t662
1266    T       t663    o369 b662
1267    B       b663    t663
1268    T       t664    o661 b663
1269    B       b664    t664
1270    P       p664    Number 341
1271  P       p471    String Tacticals  P       p471    String Tacticals
1272  O       o472    string p471  O       o472    string p471
1273  T       t472    o472  T       t472    o472
# Line 1231  Line 1276 
1276  B       b473    t473  B       b473    t473
1277  T       t474    o b465 b473  T       t474    o b465 b473
1278  B       b474    t474  B       b474    t474
 T       t475    o471 b474  
 B       b475    t475  
 T       t476    o369 b475  
 B       b476    t476  
 T       t477    o470 b476  
 B       b477    t477  
1279  P       p477    Number 367  P       p477    Number 367
1280  P       p478    Number 391  O       o664    location p664 p477
1281  O       o478    location p477 p478  O       o665    str_open p664 p477
1282  O       o479    str_open p477 p478  T       t665    o665 b474
1283    B       b665    t665
1284    T       t666    o369 b665
1285    B       b666    t666
1286    T       t670    o664 b666
1287    B       b670    t670
1288    P       p670    Number 368
1289  P       p479    String Sequent  P       p479    String Sequent
1290  O       o480    string p479  O       o480    string p479
1291  T       t480    o480  T       t480    o480
# Line 1249  Line 1294 
1294  B       b481    t481  B       b481    t481
1295  T       t482    o b465 b481  T       t482    o b465 b481
1296  B       b482    t482  B       b482    t482
 T       t483    o479 b482  
 B       b483    t483  
 T       t484    o369 b483  
 B       b484    t484  
 T       t485    o478 b484  
 B       b485    t485  
1297  P       p485    Number 392  P       p485    Number 392
1298  P       p486    Number 422  O       o670    location p670 p485
1299  O       o486    location p485 p486  O       o671    str_open p670 p485
1300  O       o487    str_open p485 p486  T       t671    o671 b482
1301    B       b671    t671
1302    T       t672    o369 b671
1303    B       b672    t672
1304    T       t673    o670 b672
1305    B       b673    t673
1306    P       p673    Number 393
1307  P       p487    String Conversionals  P       p487    String Conversionals
1308  O       o488    string p487  O       o488    string p487
1309  T       t488    o488  T       t488    o488
# Line 1267  Line 1312 
1312  B       b489    t489  B       b489    t489
1313  T       t490    o b465 b489  T       t490    o b465 b489
1314  B       b490    t490  B       b490    t490
 T       t491    o487 b490  
 B       b491    t491  
 T       t492    o369 b491  
 B       b492    t492  
 T       t493    o486 b492  
 B       b493    t493  
1315  P       p493    Number 423  P       p493    Number 423
1316  P       p494    Number 433  O       o673    location p673 p493
1317  O       o494    location p493 p494  O       o674    str_open p673 p493
1318  O       o495    str_open p493 p494  T       t674    o674 b490
1319    B       b674    t674
1320    T       t675    o369 b674
1321    B       b675    t675
1322    T       t676    o673 b675
1323    B       b676    t676
1324    P       p676    Number 424
1325  O       o496    string p131  O       o496    string p131
1326  T       t496    o496  T       t496    o496
1327  B       b496    t496  B       b496    t496
1328  T       t497    o b496 b4  T       t497    o b496 b4
1329  B       b497    t497  B       b497    t497
 T       t498    o495 b497  
 B       b498    t498  
 T       t499    o369 b498  
 B       b499    t499  
 T       t500    o494 b499  
 B       b500    t500  
1330  P       p500    Number 434  P       p500    Number 434
1331  P       p501    Number 442  O       o676    location p676 p500
1332  O       o501    location p500 p501  O       o677    str_open p676 p500
1333  O       o502    str_open p500 p501  T       t677    o677 b497
1334    B       b677    t677
1335    T       t678    o369 b677
1336    B       b678    t678
1337    T       t679    o676 b678
1338    B       b679    t679
1339    P       p679    Number 435
1340    P       p680    Number 443
1341    O       o680    location p679 p680
1342    O       o681    str_open p679 p680
1343  O       o503    string p129  O       o503    string p129
1344  T       t503    o503  T       t503    o503
1345  B       b503    t503  B       b503    t503
1346  T       t504    o b503 b4  T       t504    o b503 b4
1347  B       b504    t504  B       b504    t504
1348  T       t505    o502 b504  T       t681    o681 b504
1349  B       b505    t505  B       b681    t681
1350  T       t506    o369 b505  T       t682    o369 b681
1351  B       b506    t506  B       b682    t682
1352  T       t507    o501 b506  T       t683    o680 b682
1353  B       b507    t507  B       b683    t683
1354  P       p507    Number 444  P       p683    Number 445
 P       p508    Number 461  
 O       o508    location p507 p508  
 O       o509    str_open p507 p508  
1355  O       o510    string p119  O       o510    string p119
1356  T       t510    o510  T       t510    o510
1357  B       b510    t510  B       b510    t510
1358  T       t511    o b510 b4  T       t511    o b510 b4
1359  B       b511    t511  B       b511    t511
 T       t512    o509 b511  
 B       b512    t512  
 T       t513    o369 b512  
 B       b513    t513  
 T       t514    o508 b513  
 B       b514    t514  
1360  P       p514    Number 462  P       p514    Number 462
1361  P       p515    Number 483  O       o683    location p683 p514
1362  O       o515    location p514 p515  O       o684    str_open p683 p514
1363  O       o516    str_open p514 p515  T       t684    o684 b511
1364    B       b684    t684
1365    T       t685    o369 b684
1366    B       b685    t685
1367    T       t686    o683 b685
1368    B       b686    t686
1369    P       p686    Number 463
1370    P       p687    Number 484
1371    O       o687    location p686 p687
1372    O       o688    str_open p686 p687
1373  O       o517    string p121  O       o517    string p121
1374  T       t517    o517  T       t517    o517
1375  B       b517    t517  B       b517    t517
1376  T       t518    o b517 b4  T       t518    o b517 b4
1377  B       b518    t518  B       b518    t518
1378  T       t519    o516 b518  T       t688    o688 b518
1379  B       b519    t519  B       b688    t688
1380  T       t520    o369 b519  T       t689    o369 b688
1381  B       b520    t520  B       b689    t689
1382  T       t521    o515 b520  T       t690    o687 b689
1383  B       b521    t521  B       b690    t690
1384  P       p521    Number 485  P       p690    Number 544
1385  P       p522    Number 521  P       p691    Number 580
1386  O       o522    location p521 p522  O       o691    location p690 p691
1387  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1388  P       p523    String inv_image  P       p523    String inv_image
1389  O       o523    opname p523  O       o523    opname p523
# Line 1363  Line 1411 
1411  B       b530    t530  B       b530    t530
1412  T       t531    o523 b530  T       t531    o523 b530
1413  B       b531    t531  B       b531    t531
1414  T       t532    o522 b531  T       t691    o691 b531
1415  B       b532    t532  B       b691    t691
1416  P       p532    Number 553  P       p692    Number 582
1417  P       p533    Number 751  P       p693    Number 680
1418  O       o533    location p532 p533  O       o693    location p692 p693
1419    NSummary!rewrite        rewrite rewrite Summary
1420    P       p694    String unfold_inv_image
1421    O       o694    rewrite p694
1422    NCzf_itt_set_bvd        Czf_itt_set_bvd Czf_itt_set_bvd NIL
1423    NCzf_itt_set_bvd!setbvd_prop    setbvd_prop     setbvd_prop Czf_itt_set_bvd
1424    O       o695    setbvd_prop
1425  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1426  P       p534    String inv_image_df  P       p534    String inv_image_df
1427  O       o534    dform p534  O       o534    dform p534
# Line 1414  Line 1468 
1468  B       b545    t545  B       b545    t545
1469  T       t546    o543 b525  T       t546    o543 b525
1470  B       b546    t546  B       b546    t546
 P       p546    String "| "  
 O       o546    string541 p546  
 T       t547    o546  
 B       b547    t547  
1471  B       b548    t539  B       b548    t539
1472  T       t548    o543 b548  T       t548    o543 b548
1473  B       b549    t548  B       b549    t548
# Line 1450  Line 1500 
1500  B       b559    t558  B       b559    t558
1501  T       t559    o b549 b559  T       t559    o b549 b559
1502  B       b560    t559  B       b560    t559
 T       t560    o b547 b560  
 B       b561    t560  
 T       t561    o b546 b561  
 B       b562    t561  
 T       t562    o b545 b562  
 B       b563    t562  
 T       t563    o b544 b563  
 B       b564    t563  
 T       t564    o b543 b564  
 B       b565    t564  
 T       t565    o b542 b565  
 B       b566    t565  
 T       t566    o b541 b566  
 B       b567    t566  
 T       t567    o540 b567  
 B       b568    t567  
 T       t568    o534 b538 b540 b568  
 B       b569    t568  
 T       t569    o533 b569  
 B       b570    t569  
 P       p570    Number 790  
 P       p571    Number 1045  
 O       o571    location p570 p571  
1503  NSummary!rule   rule    rule Summary  NSummary!rule   rule    rule Summary
1504  P       p572    String inv_image_isset  P       p572    String inv_image_isset
1505  O       o572    rule p572  O       o572    rule p572
# Line 1537  Line 1564 
1564  B       b590    t590  B       b590    t590
1565  T       t591    o574 b579 b590  T       t591    o574 b579 b590
1566  B       b591    t591  B       b591    t591
 NSummary!incomplete     incomplete      incomplete Summary  
 O       o591    incomplete  
 T       t592    o591  
 B       b592    t592  
1567  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
 P       p592    Number 821  
 P       p593    Number 829  
 O       o593    resource_defs p592 p593 p264  
1568  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
 P       p594    Number 827  
 O       o594    uid p594 p593  
1569  P       p595    String []  P       p595    String []
1570  O       o595    uid p595  O       o595    uid p595
1571  T       t595    o595  T       t595    o595
1572  B       b595    t595  B       b595    t595
 T       t596    o594 b595  
 B       b596    t596  
 T       t597    o b596 b4  
 B       b597    t597  
 T       t598    o593 b597  
 B       b598    t598  
 T       t599    o b598 b4  
 B       b599    t599  
 T       t600    o572 b574 b591 b592 b599  
 B       b600    t600  
 T       t601    o571 b600  
 B       b601    t601  
 P       p601    Number 1047  
 P       p602    Number 1498  
 O       o602    location p601 p602  
1573  P       p603    String inv_image_member_intro  P       p603    String inv_image_member_intro
1574  O       o603    rule p603  O       o603    rule p603
1575  P       p604    Var y  P       p604    Var y
# Line 1591  Line 1594 
1594  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1595  NCzf_itt_member!mem     mem     mem Czf_itt_member  NCzf_itt_member!mem     mem     mem Czf_itt_member
1596  O       o608    mem  O       o608    mem
1597    T       t695    o608 b582 b529
1598    B       b695    t695 x
1599    T       t696    o695 b525 b695
1600    B       b696    t696
1601    NSummary!prim   prim    prim Summary
1602    O       o696    prim
1603    T       t697    o696 b4
1604    B       b697    t697
1605    T       t698    o694 b530 b696 b697 b4
1606    B       b698    t698
1607    T       t699    o693 b698
1608    B       b699    t699
1609    P       p699    Number 682
1610    P       p700    Number 764
1611    O       o700    location p699 p700
1612    NOcaml!str_let  str_let str_let Ocaml
1613    O       o701    str_let p699 p700
1614    NOcaml!patt_var patt_var        patt_var Ocaml
1615    P       p701    Number 686
1616    P       p702    Number 700
1617    O       o702    patt_var p701 p702
1618    NOcaml!patt_done        patt_done       patt_done Ocaml
1619    O       o703    patt_done p699 p700
1620    T       t703    o703
1621    B       b703    t703 fold_inv_image
1622    T       t704    o702 b703
1623    B       b704    t704
1624    NOcaml!apply    apply   apply Ocaml
1625    P       p704    Number 703
1626    O       o704    apply p704 p700
1627    P       p705    Number 747
1628    O       o705    apply p704 p705
1629    NOcaml!lid      lid     lid Ocaml
1630    P       p706    Number 712
1631    O       o706    lid p704 p706
1632    P       p707    String makeFoldC
1633    O       o707    lid p707
1634    T       t707    o707
1635    B       b707    t707
1636    T       t708    o706 b707
1637    B       b708    t708
1638    P       p708    Number 713
1639    O       o708    apply p708 p705
1640    NOcaml!proj     proj    proj Ocaml
1641    O       o709    proj p708 p705
1642    O       o710    uid p708 p705
1643    P       p710    String Ml_term
1644    O       o711    uid p710
1645    T       t711    o711
1646    B       b711    t711
1647    T       t712    o710 b711
1648    B       b712    t712
1649    O       o712    lid p708 p705
1650    P       p712    String term_of_string
1651    O       o713    lid p712
1652    T       t713    o713
1653    B       b713    t713
1654    T       t714    o712 b713
1655    B       b714    t714
1656    T       t715    o709 b712 b714
1657    B       b715    t715
1658    P       p715    String "MP-Caml3.02 term:\\132\\149\\166\\190\\000\\000\\000m\\000\\000\\000+\\000\\000\\000{\\000\\000\\000w\\160\\160\\160$\\000\\000\\000\\000\\160)inv_image\\1601Czf_itt_inv_image@@\\160\\160@\\160\\160\\160\\004\\n\\160#var@\\160\\148!s@@\\160\\160\\160!x@\\160\\160\\004\\012\\160\\148!a@\\160\\160@\\160\\160\\160\\004\\029\\004\\019\\160\\148!x@@@\\160\\160@\\160\\160\\160\\004%\\004\\027\\160\\148!t@@@"
1659    O       o715    string p708 p705 p715
1660    T       t716    o715
1661    B       b716    t716
1662    T       t717    o708 b715 b716
1663    B       b717    t717
1664    T       t718    o705 b708 b717
1665    B       b718    t718
1666    P       p718    Number 748
1667    O       o718    lid p718 p700
1668    O       o719    lid p694
1669    T       t719    o719
1670    B       b719    t719
1671    T       t720    o718 b719
1672    B       b720    t720
1673    T       t721    o704 b718 b720
1674    B       b721    t721
1675    T       t722    o701 b704 b721
1676    B       b722    t722
1677    T       t723    o b722 b4
1678    B       b723    t723
1679    T       t724    o701 b723
1680    B       b724    t724
1681    T       t725    o369 b724
1682    B       b725    t725
1683    T       t726    o700 b725
1684    B       b726    t726
1685    P       p726    Number 766
1686    P       p727    Number 969
1687    O       o727    location p726 p727
1688    P       p728    String " | "
1689    O       o728    string541 p728
1690    T       t728    o728
1691    B       b728    t728
1692    T       t729    o b728 b560
1693    B       b729    t729
1694    T       t730    o b546 b729
1695    B       b730    t730
1696    T       t731    o b545 b730
1697    B       b731    t731
1698    T       t732    o b544 b731
1699    B       b732    t732
1700    T       t733    o b550 b732
1701    B       b733    t733
1702    T       t734    o b543 b733
1703    B       b734    t734
1704    T       t735    o b542 b734
1705    B       b735    t735
1706    T       t736    o b541 b735
1707    B       b736    t736
1708    T       t737    o540 b736
1709    B       b737    t737
1710    T       t738    o534 b538 b540 b737
1711    B       b738    t738
1712    T       t739    o727 b738
1713    B       b739    t739
1714    P       p739    Number 1007
1715    P       p740    Number 1262
1716    O       o740    location p739 p740
1717    NSummary!interactive    interactive     interactive Summary
1718    O       o741    interactive
1719    NSummary!ext_rule       ext_rule        ext_rule Summary
1720    P       p741    String "rwh unfold_inv_image 0 thenT autoT"
1721    O       o742    ext_rule p741
1722    NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1723    O       o743    status_incomplete
1724    T       t743    o743
1725    B       b743    t743
1726    NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1727    O       o744    ext_unjustified
1728    NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1729    P       p744    String main
1730    O       o745    tactic_arg p744
1731    NSummary!msequent       msequent        msequent Summary
1732    O       o746    msequent
1733    T       t746    o b583 b4
1734    B       b746    t746
1735    T       t747    o b580 b746
1736    B       b747    t747
1737    T       t748    o b578 b747
1738    B       b748    t748
1739    T       t749    o746 b587 b748
1740    B       b749    t749
1741    NSummary!parent_none    parent_none     parent_none Summary
1742    O       o749    parent_none
1743    T       t750    o749
1744    B       b750    t750
1745    T       t751    o745 b749 b4 b750
1746    B       b751    t751
1747    T       t752    o744 b751 b4
1748    B       b752    t752
1749    T       t753    o742 b743 b752 b4 b4
1750    B       b753    t753
1751    T       t754    o741 b753
1752    B       b754    t754
1753    P       p754    Number 1038
1754    P       p755    Number 1046
1755    O       o755    resource_defs p754 p755 p264
1756    P       p756    Number 1044
1757    O       o756    uid p756 p755
1758    T       t756    o756 b595
1759    B       b756    t756
1760    T       t757    o b756 b4
1761    B       b757    t757
1762    T       t758    o755 b757
1763    B       b758    t758
1764    T       t759    o b758 b4
1765    B       b759    t759
1766    T       t760    o572 b574 b591 b754 b759
1767    B       b760    t760
1768    T       t761    o740 b760
1769    B       b761    t761
1770    P       p761    Number 1264
1771    P       p762    Number 1715
1772    O       o762    location p761 p762
1773  T       t609    o608 b604 b525  T       t609    o608 b604 b525
1774  S       s609    t586 h  S       s609    t586 h
1775  G       s609    t609  G       s609    t609
# Line 1625  Line 1804 
1804  B       b621    t621  B       b621    t621
1805  T       t622    o574 b606 b621  T       t622    o574 b606 b621
1806  B       b622    t622  B       b622    t622
1807  P       p622    Number 1085  T       t762    o b612 b4
1808  P       p623    Number 1093  B       b762    t762
1809  O       o623    resource_defs p622 p623 p264  T       t763    o b609 b762
1810  P       p624    Number 1091  B       b763    t763
1811  O       o624    uid p624 p623  T       t764    o b607 b763
1812  T       t624    o624 b595  B       b764    t764
1813  B       b624    t624  T       t765    o b583 b764
1814  T       t625    o b624 b4  B       b765    t765
1815  B       b625    t625  T       t766    o b580 b765
1816  T       t626    o623 b625  B       b766    t766
1817  B       b626    t626  T       t767    o b578 b766
1818  T       t627    o b626 b4  B       b767    t767
1819  B       b627    t627  T       t768    o b605 b767
1820  T       t628    o603 b574 b622 b592 b627  B       b768    t768
1821  B       b628    t628  T       t769    o746 b614 b768
1822  T       t629    o602 b628  B       b769    t769
1823  B       b629    t629  T       t770    o745 b769 b4 b750
1824  P       p629    Number 1500  B       b770    t770
1825  P       p630    Number 2330  T       t771    o744 b770 b4
1826  O       o630    location p629 p630  B       b771    t771
1827    T       t772    o742 b743 b771 b4 b4
1828    B       b772    t772
1829    T       t773    o741 b772
1830    B       b773    t773
1831    P       p773    Number 1302
1832    P       p774    Number 1310
1833    O       o774    resource_defs p773 p774 p264
1834    P       p775    Number 1308
1835    O       o775    uid p775 p774
1836    T       t775    o775 b595
1837    B       b775    t775
1838    T       t776    o b775 b4
1839    B       b776    t776
1840    T       t777    o774 b776
1841    B       b777    t777
1842    T       t778    o b777 b4
1843    B       b778    t778
1844    T       t779    o603 b574 b622 b773 b778
1845    B       b779    t779
1846    T       t780    o762 b779
1847    B       b780    t780
1848  P       p631    String inv_image_member_elim  P       p631    String inv_image_member_elim
1849  O       o631    rule p631  O       o631    rule p631
1850  P       p632    String J  P       p632    String J
# Line 1690  Line 1890 
1890  B       b645    s644  B       b645    s644
1891  T       t645    o575 b645  T       t645    o575 b645
1892  B       b646    t645  B       b646    t645
1893  S       s646    t586 h h634 h635  H       h322    v t609
 G       s646    t609  
 B       b647    s646  
 T       t647    o575 b647  
 B       b648    t647  
1894  H       h648    w t612  H       h648    w t612
1895  P       p648    Var C  P       p648    Var C
1896  O       o648    var p648  O       o648    var p648
1897  T       t648    o648 b527  T       t648    o648 b527
1898  S       s648    t586 h h634 h635 h648  S       s322    t586 h h634 h635 h322 h648
1899  G       s648    t648  G       s322    t648
1900  B       b649    s648  B       b327    s322
1901  T       t649    o575 b649  T       t327    o575 b327
1902  B       b650    t649  B       b331    t327
1903  S       s650    t586 h h634 h635  S       s650    t586 h h634 h635
1904  G       s650    t648  G       s650    t648
1905  B       b651    s650  B       b651    s650
1906  T       t651    o575 b651  T       t651    o575 b651
1907  B       b652    t651  B       b652    t651
1908  T       t652    o574 b650 b652  T       t331    o574 b331 b652
1909  B       b653    t652  B       b332    t331
1910  T       t653    o574 b648 b653  T       t332    o574 b646 b332
1911  B       b654    t653  B       b335    t332
1912  T       t654    o574 b646 b654  T       t335    o574 b644 b335
1913  B       b655    t654  B       b339    t335
1914  T       t655    o574 b644 b655  T       t339    o574 b640 b339
1915  B       b656    t655  B       b340    t339
1916  T       t656    o574 b640 b656  T       t340    o574 b638 b340
1917  B       b657    t656  B       b359    t340
1918  T       t657    o574 b638 b657  T       t359    o574 b636 b359
1919  B       b658    t657  B       b368    t359
 T       t658    o574 b636 b658  
 B       b659    t658  
 P       p659    Number 1537  
 P       p660    Number 1544  
 O       o660    resource_defs p659 p660 p236  
 P       p661    Number 1542  
 O       o661    uid p661 p660  
 T       t661    o661 b595  
 B       b661    t661  
 T       t662    o b661 b4  
 B       b662    t662  
 T       t663    o660 b662  
 B       b663    t663  
 T       t664    o b663 b4  
 B       b664    t664  
 T       t665    o631 b634 b659 b592 b664  
 B       b665    t665  
 T       t666    o630 b665  
 B       b666    t666  
1920  O       o666    location p p  O       o666    location p p
1921    P       p780    String "assertT << (mem{'y; 's} & mem{'a['y]; 't}) >> thenT autoT thenT copyHypT 2 2 thenT rwh unfold_inv_image 3 thenT dT 3 thenT autoT"
1922    O       o780    ext_rule p780
1923    T       t781    o b327 b4
1924    B       b781    t781
1925    T       t782    o b645 b781
1926    B       b782    t782
1927    T       t783    o b643 b782
1928    B       b783    t783
1929    T       t784    o b639 b783
1930    B       b784    t784
1931    T       t785    o b637 b784
1932    B       b785    t785
1933    T       t786    o b635 b785
1934    B       b786    t786
1935    T       t787    o746 b651 b786
1936    B       b787    t787
1937    T       t788    o745 b787 b4 b750
1938    B       b788    t788
1939    T       t789    o744 b788 b4
1940    B       b789    t789
1941    T       t790    o780 b743 b789 b4 b4
1942    B       b790    t790
1943    T       t791    o741 b790
1944    B       b791    t791
1945    P       p791    Number 1754
1946    O       o791    resource_defs p791 p237 p236
1947    P       p792    Number 1759
1948    O       o792    uid p792 p237
1949    T       t792    o792 b595
1950    B       b792    t792
1951    T       t793    o b792 b4
1952    B       b793    t793
1953    T       t794    o791 b793
1954    B       b794    t794
1955    T       t795    o b794 b4
1956    B       b795    t795
1957    T       t796    o631 b634 b368 b791 b795
1958    B       b796    t796
1959    T       t797    o666 b796
1960    B       b797    t797
1961  NSummary!id     id      id Summary  NSummary!id     id      id Summary
1962  P       p666    Number 483503177  P       p666    Number 483503177
1963  O       o667    id p666  O       o667    id p666
# Line 1750  Line 1967 
1967  B       b668    t668  B       b668    t668
1968  T       t669    o b668 b4  T       t669    o b668 b4
1969  B       b669    t669  B       b669    t669
1970  T       t670    o b666 b669  T       t798    o b797 b669
1971  B       b670    t670  B       b798    t798
1972  T       t671    o b629 b670  T       t799    o b780 b798
1973  B       b671    t671  B       b799    t799
1974  T       t672    o b601 b671  T       t800    o b761 b799
1975  B       b672    t672  B       b800    t800
1976  T       t673    o b570 b672  T       t801    o b739 b800
1977  B       b673    t673  B       b801    t801
1978  T       t674    o b532 b673  T       t802    o b726 b801
1979  B       b674    t674  B       b802    t802
1980  T       t675    o b521 b674  T       t803    o b699 b802
1981  B       b675    t675  B       b803    t803
1982  T       t676    o b514 b675  T       t804    o b691 b803
1983  B       b676    t676  B       b804    t804
1984  T       t677    o b507 b676  T       t805    o b690 b804
1985  B       b677    t677  B       b805    t805
1986  T       t678    o b500 b677  T       t806    o b686 b805
1987  B       b678    t678  B       b806    t806
1988  T       t679    o b493 b678  T       t807    o b683 b806
1989  B       b679    t679  B       b807    t807
1990  T       t680    o b485 b679  T       t808    o b679 b807
1991  B       b680    t680  B       b808    t808
1992  T       t681    o b477 b680  T       t809    o b676 b808
1993  B       b681    t681  B       b809    t809
1994  T       t682    o b469 b681  T       t810    o b673 b809
1995  B       b682    t682  B       b810    t810
1996  T       t683    o b462 b682  T       t811    o b670 b810
1997  B       b683    t683  B       b811    t811
1998  T       t684    o b455 b683  T       t812    o b664 b811
1999  B       b684    t684  B       b812    t812
2000  T       t685    o b446 b684  T       t813    o b661 b812
2001  B       b685    t685  B       b813    t813
2002  T       t686    o b437 b685  T       t814    o b657 b813
2003  B       b686    t686  B       b814    t814
2004  T       t687    o b428 b686  T       t815    o b654 b814
2005  B       b687    t687  B       b815    t815
2006  T       t688    o b419 b687  T       t816    o b649 b815
2007  B       b688    t688  B       b816    t816
2008  T       t689    o b410 b688  T       t817    o b631 b816
2009  B       b689    t689  B       b817    t817
2010  T       t690    o b401 b689  T       t818    o b628 b817
2011  B       b690    t690  B       b818    t818
2012  T       t691    o b392 b690  T       t819    o b625 b818
2013  B       b691    t691  B       b819    t819
2014  T       t692    o b382 b691  T       t820    o b602 b819
2015  B       b692    t692  B       b820    t820
2016  T       t693    o b375 b692  T       t821    o b599 b820
2017  B       b693    t693  B       b821    t821
2018  T       t694    o b367 b693  T       t822    o b596 b821
2019  B       b694    t694  B       b822    t822
2020  T       t695    o b358 b694  T       t823    o b572 b822
2021    B       b823    t823
2022    T       t824    o b533 b823
2023    B       b824    t824
2024    T       t825    o b358 b824

Legend:
Removed from v.3566  
changed lines
  Added in v.3567

  ViewVC Help
Powered by ViewVC 1.1.26