PVS Bug 978
Synopsis: circular proofchains
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: closed
Class: sw-bug
Arrival-Date: Wed Jan 10 15:10:01 2007
Originator: Hendrik Tews
Organization: cs.ru.nl
Release: PVS 4.0
Environment:
System:
Architecture:
Description:
--g4AlWPTQws
Content-Type: text/plain; charset=us-ascii
Content-Description: message body text
Content-Transfer-Encoding: 7bit
Hi,
I get the following from status-proofchain
***Warning***: The proof chain for data_type_length is CIRCULAR in the follow
ing:
General.Byte
See README for how to reproduce.
Bye,
Hendrik
--g4AlWPTQws
Content-Type: application/octet-stream
Content-Disposition: attachment;
filename="circular.tar.gz"
Content-Transfer-Encoding: base64
H4sIAPhvpUUAA+19+XfbOJJw/2r9FVjn+a3UUdyWnGPG3emskzg93sk1OaZ7Ns+PQ0mUzZgiFZKy
456d//2rAwABEjykOD2981nvxZFIoFCoC4VCAZiG6XQV+el333y9zx58Hty7h/8/uH93BP+P9kYP
RvRcfr4Z7d27Nxrff/Dg7t1v9kaj8d0H34h7XxEn/VlluZ8K8U0eXGZN5bKk8fX/1c9U8d+fZHnq
T3Nv5uf+7vLiGnuLDL6PfHXz/96D8V3N//27Y+D/3XsPgP9714dC/ef/c/73eu/jMM6DdJkGeTDz
ngL3xYF4dxYk6VXvcXAaxj0hjhfLJM3D+FQcH+6Pe/DEroUy4+VXywCr4n8PoYgQH271trLwV3wa
+/mwt3XhR+HsEfz8EIVZ/uHxVR6cDMXhbJYGWSbu/CgmSRKdUN1bJ9jMyt0Mgnj95ujphxo0TiQC
z/3FZOb3V+Eshxo1hQfioEelheg/S1I/ivoRlDYxRJJILKG06G3FSS6iID7Nz/rRQDwU2EtqZoC0
isIg623J3vLjfjT0seAzP8qCAba3I5ZpkswFyF++ysTBnQH2t0DLY/jQ3PNgsfAFoSjxkx3q15Fn
MBRtXeAOV1GU6Nf0rtc7imeiKjK9Xu+49OiDEiXiR0mkUKZevH715t3xy58c4LRMeO/zMKLSnaRN
yE8zw4e6XJ54EyAPCqTVLIpiQbyTosI8TRa6So0MR+E8J3AnpiQ72b0j3Pzz3j15MsLePXkiXk2i
8NTPw4So1qwOTiqVlIFJ4yyJmiAJWCNYWPvvLOeHL59qsuwI6PwqygV0UNE0zFi6RN8HkTnzlUiR
NA1KCjcDlJgDtpzqFkxJRSQGg75siH71ZyC7UHnAeBmIFRyb+2GUiSQGGjJiWb6az9fS/CZ0Imxe
HD97Bpq/Wj7q64b7UrkQO0AvnrnRA3rlZwEQaZ4jhkGaBQY5jSpitGtUmyWgrGiOsHvYO0V/5gjY
oR0W9TNoYJ5EUXKZUXVqDRh8ESYgj/llAiVV4Va2yHIoKdWuuhlT4YwY7xIOUnRk/zN/EawtHLPk
Mu6GBVizmRiIHiKyTL6qDtVrkKk8tYI3gn/jmv7WiN+I5K/m5Xgw6LEhylYTsp4fV7PTYBHEICT0
HMk/D9MsR2kQfhpgF1ZBHl4E0ZVIw9OzfCgmq5xeocj502mwhO6JSTD1VyCvBAaFFhm5mqTBNElR
z9LVNF+lQc9t8sLMq9ob6Pl/K/yoGpCqZrATb98/fve310feq2cNQ6I0wsDzcNaxPVtA1munauyp
6cxrabil2dpGqVUcLcP8CtV6Fk79PCDOsrT+Fdzc2upC+CBmspSUOHi48D/bz4TgQchbBAsYzUma
h1h1CEXRr0AHDnSMoN0uHAeWQ/HDQwQpQUwiAAh4mKCo4hCGDDn8p358GijNlDicDIqGiGAgaVmQ
P9KVJlEyPe8zpBIGA25Bg2Z7jEAaMfaiMA78tJa1tU6bU7nd/pdWVcSkxQ/jsuyMlf2uXm8d/1/P
/6ZJDF0CW3C9cz/8tMz/7t+7Ny7mfw9o/rc3Ht/M/36Lz444DeIAhFRoARDor6EwZ6K3gyZjGq1m
OPfz0+lZmAdkysUsWAbxDGwW+BxBBrL4k4SjPf0du0IYF1UcbTnmmi9Xi0mQeq/TZEl2bBLmmbeE
J9IBXyYZTCvxzQLNSektvAKV+UOlogeFw8VqgUPr5xD8ILvijw+r0HpsCm3Iwedl3h8P7er11n9H
oO7XO/aPGfZLoOZimV95PLGBkRUctr5qfICUy33oAJBnr7YtNKxefuaDmS6wtgxSzN1QTkUsftD9
+UNhe/CxgtADforD9+9eeW+Ofn5z/O7ojn7lgRWD1ztMpEsc8g0ijfuj+wPrLZbXCOkqDwUYgv37
VPJnhlFPDKxRIsbOjq7qXQRTPTcUE/j1YXT/RJWodgKhDS302LRKkcbJ7eH+uFayO8q1nu9qsLWi
oma/tdKyQ8DR1ZLDGXALZljKs4PnQP8VqmNMSoSD+WSVeZcwcJxp7uyPpWDz8GZzTRcf1OFZ1Kxw
VAJ8KO6O/3j3j/cfjP94366A0lZfS8ni/hjbUb5Hk0BwVZd+kFdL8x58WPF90R1Nk9lqGuDcMAAq
LoGtQEFdmcoHn1ZMfHYNNU4PFRIlmjHR8oQgvP7rW4YyPQum50G6K45zmBHHM1BUZO5/Zsppnifp
QjXx7NWbw+fPyY8pZgEH7Kj80JVHytvB4l7RacPn1F0x3MyaLlEjJNlyoob4KmYxr9qQyDdAQonC
gI1MIfsgrTA3AdEBZQTWofLKEpdAaz8WfpQlQHRyImkCDMyGmQ3abDAKOSAvy/fDORfI/AtUJTEP
LhH8eHKBIoWzcWB+VtixRdXMGcywSlXEfCHtnaEbQKQXl21GzynjsqKHLj904wC7OGD3mEz7Q7GH
TmyIU074+4PlzkqLyBCqRlP3qMZ26vdDA+qwZBeGUHFLd3to06W3EUjGRrIObLL2YZarFJwCDCmc
greNZg/LvJG/7Jgh91oCmYUghcTi3d1deqZAeDG5CsznB/YrGvyKADey1C5gm1uD8lKOAfUY1ChD
Q4GT6YxiIAvRxzf74zsgp7JAEsMUXE6zlYyfBTEWv6L5ODyfoRxG4TTMoWyOb6kWjAsSlCbLwKJL
VtDkH0eHvwzF0WP88wT/PKU/x/DnLf55/PqfNkn9FttskfFbB+kQFRmWAJMRTtF+ICFAN/vwT+r2
wBhk5wEObUFGlfrQu2SJTJ8pazu7ApIBIFUOHgL5TxNWfijBBlZZDWw2YNP1M1gNGCnQ/hMbQrAg
QgYxfGINEBqJ/WkFgz+8i5Jc20RCH1SSaoKPJWuAvyCWfgpMhG6TUQIuJgtsKZ6vMqiBvgG4F57G
V3Pjwy01TwSzenaVwZQ+Ejxdls9RpJaLIkpEyFz4YeTD7LpSRwO7CNN85Xj+5M0eekriDnT9LESR
yVbg2l6EyI7LNKQOEhlB3FKRfpdA306JFQQAiwRgihJ0jeQkfSg0/GUWwBiQs6bp19js3Q93sdUg
JrzfYqMWYPxzB6iHLDvV4PzcDe71++On/RFJ70D2B6EJP8/TcLLKeTLyWQN/9/yxTdad5WkVU1EF
vY+gT6NkgrYH8S2I3+PAP0/RcdHsXz3Tc3/0/J/7f/2T/2/a5v/3Hozv3dPz/3t3H8D8f39/f+9m
/v9bfHo9c6XNsfKrZy1q5Xfnyz4IgW2mtFgUrcvU4y8Erp32LMhLsyNymx+C0f7BjPUZ3mkRNizs
KQcQ9WTZjkOChTYXBUorrEWD6HmVm62f+1noeBzb9EZNU0EYh8i3jINgBsNgSF4BmrjVFAvxSNzm
m9vNleMFjVQx46cjy8NE8Xl+fPRWmlV3oHYE1YpgrRGhNeO4I0k4mljR4o0c2zzN4j5Hqw0WlLn1
D3MBSfwvMQUr/bOWHUyVMPagOQxUK7KYdBkKq+EG4tALjih3ooxFFXeHeVbGOuTNwuxjAsMzwxmV
cRrJPAzR24IPFhmXi4wLUTcC7AzttgTyA4f3x+LVG/12LN+O1dtRM0kLXPUXJXIEk8nL6wCjoXDi
OiqjLGnpJoauQ7Bk1SJbQ68kWrVsVigYThHVIOtDgBIxkCYYcE/BCUYj9WW9HhoWrrxKoglSL1zV
HgVZsSTSVFN3t6bmWkzQ1C9zoyMGs3A+B9c8ngZ9jYyLR7q7au3EzjLp9V6QE/ThLU4JqqkrOxgP
Zz8JV6t9cOEXC7Cv8pHKoEO7vCNCjAbizO0yhClgGvgzmiWQhyzmq5jKwfy0t8OBBzlVmAVzsJy8
FB4nZL5BjFQLAADKZzh9WMmlPg3qOxoEEGJ17Db7ORQv/PPAe5f6cYbhpiBFi3p947rElToSqpDZ
9QztzB6P15Nrkn+4eY8IfiCUNmBejmQrfHtDGQf8eyg4x0cn+UgAzKgCApdrgvMeunti5fxkcvGU
CuCYtZAPrI6QZZAvikXCuiVZObjgQ1r8kMGA12rFVyQXMDPLzzAMomQVVwjn/lRNhWcJrd7LuBjN
f1UcDMQNKQeTrF3Rz4KAI2iHKjf0Dbzz3sdcc8ZRhOWCiO2t1GOdSWH1EjModnYKd0n0iRpWGTRZ
OzKzRA6wSEJJ31LyhyooxKs/PwJgfzc43/cH/WwwKMqo0baoFMP0zqO+u+viciuahGvUDJ4dI4vF
d0Rm+n6dnq/ToTQFmlps8iW7Qxg7IVSKAnUH7MhMIiTsAWjNdJVmGLh16I9U5yc+jmigFolK0IpX
ESrJqz/3QRVXUHQwVHEFXHXpT4YijdBv6ff7JhJG+wNx6xb5PiFPDIDFRlxV3BkNKGqGJYSAMilm
MlC7xWMMuYD1TM69vDCgVg/6hByXDqIssOrVVRL9Z37uR6paDCMafi3q19P19oh6TsVlPWxuIASJ
8cGBi8ycfwdD4BQJjab16PDt+zdHKt0AeNVrFwgtw5tKlAXALVBrANj/UgB3m0RalyTKoxlmFwOF
WtRLtZFGKmUbJIuMOEbmSbBIiLdYslHcmDnEexbw4ALc/nAOUtc3DZWSANCELWVUJ4AKtjboFwZO
mVAj70TiIbXAUgIDp6KgRHikNGEHFBH8riT+z5x9G8AqsCqRXTaQGGo1pS4OrMJGX4sPOEYweOUJ
NzAJzmBGa6H6ozhK0yQtVyRNssGTXtjNCUd7cmnNaAMmtN8LXENK4jyMV4FCp7dV4ku9lABJh3IC
OEJOcWOKXzCaUXErP6gPCDeyrvYDJNd1C4qrRkpUN2Vk0Nuy6YRirYwEPVQWgsMXdYpVUSuwlHZO
VI/xfNTvoFeMgT1VlhbqNOCtKp3AqOQphtCGvDHOmdhHLuxdA53gkc6FvAwEFFbWkWB2Td6G6Qgb
w06Gfl2eFbMKKvGfxOxr8kPMKSn6qda0tBKiYzm3MCQvladMeQGtJF1mDaC9NQ9FZcEYB7Xc4q/b
mb2f0OVvrGCo4tFn4HvmCvxxfManRF9wOT6B/OUJZp3mVQuu83KRKMmE87HTgCcgHNkTXdTNJIhn
T4MaYnm6OwbaqDYO4e1I/X5tTxGu7u2LBCYhSYzLlVcb9A9qO2InxfzfGxk4eWNHdERxsRRiqFQd
aDJsqaLdKOGRvd/qSjivKXZUSwigNK1QbU4JY89HEq/RNXKlu3etGL8eGqNQY33GqJYvg2udnVnz
/kaDSUWu1WJ+qUHkUeh3aRFhNFQuKRbjuLNlHtE4VmdsMF37YrNYJYtncdm1ta680mFhv5adbGVK
zTxVTDayka7O/h6MZBsZylaytTwpPriqMnakw7beE4o/fVDxIvf+w6aAqw5h2bFcR0DVDBSfDIUR
TPWO4ws/Df0YZpSJhwrSq4/8obNUjfCVooaf5O86JZRbDWUE772rDwfiaZBN03CiQoBkbsp2RnxS
2VBqT5lOnaN0lRy3CuHyogpHa1sk/F2Q1ZT2k03DLIiuDiQoTVJwpR+RjH8aZrjP9CyJZhlOLQt4
QCSVSAPYUasSShXVPEgXYYw7XMAbp2o8naWIM8g4JUAJSn0GNCUYhW1o9m7G+V61iOo9LTJ4iM7/
Jwqt4Cau4lnVr+tWyAhEElirjhCueU5DVUJzq6kSx0WN5DllW8mmHojjOUgcUIgIwvQYcjbZVbKS
U35caVY5bIlYBilyBZc81GwdRaNMV42LbXxrCV+O2X4VSlCYPic5Ai07fMMGkPUaXlmjsDGbadZF
FbxvmAT1GnT1Geal4vs7AnNY00kI70A/uAtD/c5yGDL3Y7sHPq3PWaVMb2Knyq1QWbNHWmMlBNkq
cd7nTbVUUFym+S4lwAUR7y6k5GYDDYUCBlZN7KLAv2Bjc+FHK8zZyDmRTpNSo9dzCFaBKg0YjN/Q
aqLkEhlL3EYpE5ALSLF7s7pG0eQssWzU7cTnlvoM3Wqv/4mflR2nngr5GPZIGA8bDFJjoaouyfK2
l7O+QmKIqYs+7qhcWBVxcR+VUMv/YinK5fxcC7e+WPgKLlwP43/PfBedGL8+mwuTY7L5i1ljJyGs
YxgcTvumIlznulv+/chunxz4XussT45RQ3Mu1j4RKM0DmvGw5Lt15lCU3YR33tgG19vSM5ENAY7s
2UlPbVtX0rYpT0k3knPg6tGLF4fMVdrjI/pZYZPaTJIRr7k2G9TBCGlro6pIKquqFcVXcXaequNG
IQ5VuZyBdc07wPFKrtnamkLrql0UxTwV5Qul6VplfTNJx25zXK1Fha2WiEuHsaAdHnoehS6kniv6
qzxZ4A4Omn2FYEQxYanFqxzqoyOkO0m7y0zOLlacIiEdTWsSWKhk39xdjF5trLEc7G4gYtxPU6ro
ibL7A/HqjXpiu4b69Kcv108zyCFjG6VQhzeuTVXr7Yg/4W4VR1hDZgXjcTCrFPe0CNzyGPpR+CtN
hhFGSufRUPKPLxyTFNFHhZbzdprP4Z4i0SefHqMrUz9GoaBdN6WTZjjuovgOTOkZ+yyLrTIUvqEt
NwPqjoSDNNGt4DRV7vwB/l7oQ28A1WSF037kXHmBUPhzhF9ZwOvRPp4udYrcnR3XeVYWj4YUGPHe
BnnmPecMvdp4kJp3Xu+ctMhL6zAnvaZgupQoQ/QKeZHB1+uMnr+z9vhSbiapmsqf1HitYSehePeg
5GAoyxvqq9p8RxNahU0oI3BhLoLPeLKCjD3KKEyE6pRAJygx56Cn8sbo/AUQQ+Ex+plnxN5ctowx
rulc3SxYDp2XrUFwMwxOpQeVWUJHQsN4hJvgoiAvFp+KgPilzNyiEHEKby8C+czog8vv7mzzS3Qi
x9szFeVLoufX4QJ3Y6Q3Ls/WtjaFNJL0nCZxjNv4WuFwirN7orQxH5zgmid6HUW+ZlbbMtFrNASW
LK5FPKZdg64o3wcjdiRGaM+MEd0K321C6Pq2ncIfGRtQhgZ04yG6mJXH9dqxJh9NBFzzTCdK1Vrl
ha1OlWSdYleDs7HKo4099ebRp9oOVXLg1KbRBcvR/25jSE/G/X3B+1ia4HU3xKX5nXNjTMqmeSjS
S/llkXA3G5Yu1xjxhWijuWwYKC1xMTe9rCfJCpRjv43qVVFIm6nqFpmu/WvumGpyMOyUaEhaoHfd
8ISyzJ2BAfV6czVoB0wpIENLEUaO/XX6l5dp7h4f6qTbWdiYa7hMa9XrKp8JqUPXhnS3DFu9rj6s
3CYlnasiQbEIAztC1pZd47kXHUSipsk1WZKXdpqkJnHT6hMaJpp38SsWgyCQm1uvU7hc011j9oJI
fGf26/oErZseb7iE1TF7T+ZpKWZ/iVdUD7Vxc49zumEHKBtWRJyZRGsvgNRC+dJFkQbAeGZKfWL1
2isFXyXJp6DhmrLqmJ+sC0HOS65JywsXWsaMrnO8wM1Dha3COX9yzjkURUSJHtZx25FG78xWS8tj
hnHcvjVcdB0tOiV0yrEiZTPO2/Kro4QVT8bcjutopW7hVD5jelg77dVWjrL4tW5CIFjNi5OObURy
kadpR1S9dGBlmbeRzG1ZCWPZ4c4iIzG5kZvrlZvqelcnGVpfiAj4GnLkytqTr0i4soSKYP5WJY6N
4F7pCKSM18N0kfPpMjr0ig4Tm6+ieRjxKSMXAYBWkV6KV8rcJPSWQjoJc8pHBJYOotrtlO9fosRX
lWMdgZRz6K8pzdfW1mbyu67gyo3Q5WzBYvwsFniryyPuBEBl1jRHOcVvLZ4OKb1va6tTerrOIbyW
NXMFrNZQVbPFVBX3cRYmW2tbW2fviUtcmGBVzEuttCUC6JJNIqfKlFM4nemYNaJXm9Lp9rU3Gr3r
ZXPtHc3NoNbY29xFXzbRls66sp6m9FQ6wcZyiZgVRvHTQG4HMNfSxFpOAr7f3KhWox3r66xLl4y5
Zzlrr7v1vi412lCJwOPgqX7VdTViW11mNtYeW6dgV8JhhjBPKhcqdI+GfYV4WIMwfpX2XB7spZSh
uq3FzfOflgDdGmbPtbD0BUePbAB/rXMkNoBfd8xEKR5dyXgoPG2f6nPCEt1I5VKKjRZOqhi3pEBL
M9YWe95kOaVlJaVV7hFEMS6kchlhDd377fS8ksGgo38S7dZhYV31FfJTG3aUphuGw5roY522t2ds
l0eFYipQDAvWjhAzlrGBWFccoHKY0+3+fInMdvEbbOe6kl/QQWw6h+SLFcJ6T6HLqX0Of6VGrtZJ
J60m8NQexjEwDp8029/Msb7OcaUOat1o4pr/yqPTZLKgTNta3893WO9mz6hxoXBtFVjLeXbZ7d5W
+VBdR6mKlqy3eG5K0RqNrLXmUA+3+3zky8m5trv5lf3NLxuxWqYuBTDpk+AIZh3W13kIm0Ty9PVS
ynQ5h1ru0jaT/qv51EWWr76dqpSY/WU5vdoeujNzmz1VTk/gQ1c2GF619fYkDGfqTfteuY3GW3v4
UCfHfLJHVHXQ9jqgzYiCnVXvEAq9U39n5+fUXy4BOheQXcZ1UP5Cw8HfXh+ZufY7LB1yU3U5D7z0
0DwqgKnoScgKwNSHIQA6JwWoP0WheIIPTYkyUDoZFhE381M9YPODqoG8euFP08T5flQc1tm/ZZ+o
+pDRY12cZoPS4ZmDYYGJqamNFamEPqzzltyejlyymfE7vULh//RH3/9wMQ/9bJrcWaYBJqVf50UQ
zfc/7I/37u/p+x/u7t/7Zm90b+/+g5v7H36Lzw7fxxtTltOjR73eex4A0KTjhhy5N4eGBdqg0/fP
8eyABRjccIozu4sknA30ESly/MD/Hqm74vGU4j/52Zn3JIHRM6MlxQ+Hw8fDJ46NS/JAFnEL78/p
z0L/NPVpW9lAH3WNB2srOLrhuTol5RDHp8c4qJ6qR4/x0ZOT7ymQdas/H54O+IgiNINPYHQ57c/x
HLbvectVGVeoZvzyDrMsmX74efjL8G/D/6lzFUyTX4VnoPsz4vaLhe4v+Ohv+OhMPfobPvqf+ovk
z7AJHxHTM4b+HGh4Cv/OcPykX33+KQ8/r/SpxzOxF7hf6Wl4Ec74LqKSBxQPlZ8jL990IkRXvc00
EPsAOqHu7qTj8sSPYoSzV7xuEhxIffskoSNB8DVw/lDEMJir74uGtR1Zj6+cO83LKIRD8VFY9wZ8
lLekAR5Wm+OhCAfYrsar/PojvZZuhUE79DSwdd71VRUQcFZi9gWRkEDYvc/SN4x/hbEUjzA9zUef
h/j3il/8IyXK4VvxvyJFyjXcXZHkZ+DcGVQYeVFg7j5eYJ9jujOcOsPNLciRNx7E9WQmwMtoVfCY
6kFXCM63xs94oC525LcwdVBUM8gERDOvfXWoVeGAG7QelmDUoMuXYXoZMLIiEkj8EHekWuJJdPqM
N1pDZ2Jgff8z3iMPyKfBAnP7PtcTx2zNwztZK4oAM5ahWPJBFOZ1IeIHsSxleoPW3BYTQGJJL7+F
Osi3Cfz61HDlBLRc3/6noYBJ08ehOLfbT43rYM/LByLATOBb8+1tuzj8/kjX0OOpl8Xzjw26CpT0
wOp7QPQyhhPNi6H4XA7rqRVQeLBIZv3JYHBAXJkgV4BlKVFIHkmnSHxA3JwQAQH1RqTgn4tlJZzw
wkVJOGUasFSZblJeNIKEYasMKTuWh4uqIQ0NTCQXHciE0NePzEggh35KT0xzB2VIwM/R4jVINZTx
5lGSpC67Tho0sQw8AcU0V+gw1ev7301a4GdBNG8eNiRUH6HWXzZDwNA+Oa40YjwJ4WlF5RVRpqTt
Nie5aVRHqIntS1ymqAz0fQLfO+A03hininRdG06gSbV8nRryNpFaNx1ohdyEZqIrUg5iOdGCafFk
vCluIws5fDJux3ARxl+Fl3ccvLxT5qWBwQjXXRar6Rl4g+ksSIuzFWCwW4SnZzmn3XVtQNwZ9XSa
4QKICXYLPI49geuaBA5vJ01ynDU00YdMl/QFY9fdYl+qiN86+vEt5tKvgdX1s6/ASrsOjSqIAw48
nnn7lUFQyXTNqMOD3ghbHKuhj57QD/ZU8I1yX+AFEajFbDKF6tVu4iKMUmscYAuW6KeDRnUyPFbC
IMrXFBZ0nCbWoFbPIJSSHzryBUvVD0eNKMkhXrYjpgNNFFIqIJOPitVIF6nm5CdBv7JwEjUmBtdx
1ALgoGzZvjucCVZDpPCULzd0kFZ2mTslhbEw95oW0wYng+YVY+8P9rQCjPEfEOD43v3mju7V+5Ha
d9gjyXioromvA1WRwFAThuGAIzVCOGEznEl4iltlS8BiITP1FhaCrEp4FYWedbIe0ayqFec0wPvs
O7hnzHJ6OHMo07diJn3lqVuFJlqYp8NZq/wSU+nPBrKrKzfpYcyELDrBwQULd0K3JpxQHE1+/EzS
/x0mt+3p9YcjvDpE14bhcqG35vJFGSqKT0jX2Q3WsOHUZjoHwB0G03CX2K6qRh4H+WUQxH1wALAf
fA+lBIerFHTnpZQx8b8wasc848dlvJhmZ3z9JYDDebg586abxZ4np651DgpMTCgw8bkhMCGRJM6x
+Hv5mR97i1VU4aJWBOzBP1JRBVekcRP5MaIAY9sYXZLP6OMCYWAOfweU0Wr4NE0u8c5FeR9dEF1V
bAM0euDsgSjalLPIuKDvZzW7nfDtpLFuN45iaDbw6dpzeSv6Ro2qyo/6/4gVD6vN/tNsuF9wBpE0
uc/58iquMxnGFOfBkmTP6csPongv4ttg2P5p9gqIWMO4EnfWaEApp1o3KncC5LVYEAKBJMF8HOYX
wTRPpLB+eMlYOFflzFDs5OLDyxPVowmA2PPmIV0sxp2iRzhPhYf9uQ/KPjBLj6qlR6p0nq5UYQwi
lzDkFxxbNc6C+vBOLifCf386evXmb73HRz8dv1RtqoDgO7Axvva48EkW5B/e6Z4sAlJcf1bM3fgR
qAk8xL/Fqc+yMGVtjxzl9VE+xTN5EQMexFMBMa6CmLSCaIh3yGth8W7NFbzBG7XM9WjjRlE5gBdP
JuicNCTWY6Sbk6P2ZRi0yJVSt00QjHog8oJkac4YZBTM7TVzA2jhfDqbavKBXE2lNO+qaWu6eVsM
nYxNtTsMgV4CUHIAwfMr4t3W2Wa9QxjPYzz3uSl2a480jkUFH6EEs0f9WF/kTPqtLnFmk1YKxeNo
7g/4OmcJgOvzRaF4PJ2GWk8LWcj7NUj1xmoTn/5efV2s48my1bp74Pu2t1vjKcIkMC7ddRzTdcsx
r54UGMK8b1GIQvF8jM97eMCdaooNxn+vZqd0Ure43fcPCsKB9Opf6Bz1dihdY+tPh2898i70yzAG
17RpOUY1aC0V9IwgLvLUatn4vaAwju6Hbo0jNN0a9WJ3s3ZLsd1S3NrEjm6EYzDrObZW3Q3J0tsC
Hxed9Aq/TTrd6UIn9MvYzx5b+u/ExSYUUAnPMjBWBrpIgyO+HtoSbrLCKdMcUC9W6rCYutxZGSK5
pPkcUyvZXXgn6jO8nBhzXpoXZh7eqVdGWqdfvtNbUWQiW8QRM4U3Vn7Uj5rkSbY0naVrClNRcVP0
5ERGvgNA8B5NfVH4Doba0QGgNNXgcx7EGd23EVY93AgMVjS2m5Y+XoROE7zDVSL5SGX+RSOzxbG9
5dCQETr2xahE8hjT92FITiPVH4aF3xMlMQ6khDodUgO1C3eehhiJ6klx20fElyDZJET80PJqwjia
sKGrAciFQ4EhjNpUNZnPM8rJlAC4eQM2FuDUS+r3m6Mn79+8Pf7rkcJRp2+FcwKDV43KJ3zOwCqK
lLuOV28qAtOFkUS5ocA2wOKYOAm8axbh3YEhJtL3K/O1kfjduEW21KfSJZAO0eQWzW5rgSm6a1G9
sr1UvrHIiDQq5Fhhdfj+3SvvzdHPb47fHd0u4VjGvEXMnT0AU9S1EzgXD2FehC/KHYpreoOWTsk4
t3o7LG67Zhcdrxu2BXEoyCdrlpjjZ2WJgYnJS1Nijp6/PWJJwbiV2QzedJprsTh6+fT4WZ1YSGul
q1fIWkVaaSRTzmqYmpUcLvzSwuD3KkOAN9aDwFC8Vho6T5OFeDcUf1EGof96cOIaJAI8+wDnEpQT
1W5vqTz87stL1bhP0AhbgZxDqn+BL8jeIt+VZG/2QQsYfXkNX/Dcp6F4hjPUkz5Df33S/wtVd5IA
E5+BgvT0pZ8bb9xzZlaBPA2neXTlJbigFMhEbd0/9MhtaZLHUTGn6EgIEfERz0qi+RpvnCwPbbMT
Dvn+bnebaaSGAtrfKyld5PCoieZHgqLGW9Srj0oc1WXXJJGBn63SoGrB6ZBEXILAAzdJMPsHfLr4
Z8y4xa0sdPfh7u6uGKoXsXyBc42BBBPG4vIsnJ4x69VdOGKm7+FS9yedBSKl8zoEAwsJtvrOW33g
y52RUQGFJpxiLnaceAk0EPlLOlkYyIr7CTNcBWT8h3QxFhBdVudXKfSfDvVQk2cO8WhgBY+RyUNk
tJPTYiNWY/PqunajzRKPzRF/mFU4jQ8HDKUwm3RXep/Ihlb29ZtX/+2NqL0BntmuS5gvoDDowUdv
LH9iHtjAKTT2HemRZXFlgMqhXz1SPGwDXTbg/jLnswrlSejPk1Oybeof/N51xkwP+JDzGbhhmAEZ
BcD/D9lZAm7g+Ul/b/fuPZENFJT+9jahhyK6muZiO95mfPv97dG2yu7OzpMsXCy/FQcoUtkjsKPq
lZ9lQVr8BIzwCL5txGx7o6e8T2rbWOTjFcZlknmn+bgoiEfH4EXk25//Y7St/o62y5jJ3/3tcZfu
WDhxkFg39kj/iv1FILZ/3eZyfWh6KMaY0vQfo0GBQBosI3+KN3vDhCdK9XMUFcIXHv8KnjXWp4g0
QPi1qI4MKPfC6gf8OAMCiTv3xLgQss4ELJEQMdjmTo3MMjaD4QGmCmyH8RSNQxif8lTQX312VKKP
U2ir8fZWsd13iW0dKxUVnBqiRFx3fxqEEXSFGPFdfyLZMQBSwHeXQlDNckVR1MQb4W1OduXPyMkf
AozscTXImNpPtssMw3WmKZ60FI23xQEG/mDM2v6sFSfe+3VbtzMwatdIcUXByqIpuynXLTxK0pHf
w0x9rRNGAxWXUBUqLXvX1kq5simPrnWYNmHcc9rQWmFkq/ItUFkt1aDpUF94pFJiRv2p0REH5yQx
6ttmy+XsNUYO2nq67+wp3uJyR13RuO2ioKVj7JSIbenWToZNy3e4/tj/R7EgZS5lYQRpNPinEu/6
XkOnlg69RT8cSwLRqRHdBgibagWNuVoyK482464VTdHtZMl5UOgIHKZdpmIw/LKilgez8aCKg1Ki
sr2uPnfJDwhms/iMd/cerKUoBX/U+h72G1f4ipFVkspRABN13Pa6anONXHdr8CrMEAPfdqMCT237
VGKyk362F1LfjR+NbnQYPnRXToPyONypMzyymE127Y5LfPDpzRa8f7OP3v83CfPsOjf9GZ/m/X/j
8f27Y73/797dB9/sjcYP7o1u9v/9Fp/HwPamhVpjEQVXaSmsaSzTYhQAt43DT8qxw98DOcA/xMjD
hAPOI4oziz0ZK65PANXgPIrwW6uT7sb0aiQvCYxpcQUBQEksQRkq6p1xnXfcvHEAMcD2wiwpx/dK
HdUNWfip87yFmK5wopJj8l5otI/rViopNx4KYwmreUuDBGcvT6s29mRkmAKD8tKPVS7OcSNQJvBO
NAAX0y75VN0pFRZAM0LS3A8kOalTWYuNP27U29DOHHyta7xnrjUzB43m21sqr8OrlfRSF6lvIYZ9
zjmx1UBnj3bJPDSW8PTSY9hpMV8BcyPxUcW4K9jc5g2J5/bS/jm2WVquK1HvY3N+qJIeC6eeAUeK
6UNcCCiBpqW5EWdEUqSRkiEpS0olP7axxBLaYi+mIW+6zT1mU3N3KN+imcYG7HOTkz0H8Vpa2yk6
or+st0hbqe9aaEdcwIk7h38hynqR9SHKPLfwpzoDVYku3AYmhmPMDziXfNvrbQHXwDCHGNYC0D/q
VzYseEtwMO4R4q26xGx3GXrdRQC6d7uuy3U9dveWzaCFuoF5gTVmW52Fc8kbTIDS1prtX2xkNoRN
y/clMLTtck0ZcYHoZMPOseuh2kptbMm8g12xrYa7u+a2z1bTZoAwjvB02TfLyH4sYWIaVAdWTRtH
d1y4cPL7hpk4FTgd+/UjPLIsdQhE/+iw1t16a6KBGX9laawOvA00wuUVPi6pzWDZJWm3gRpT6L0M
RGTKn9BeBK2bhrTmlaQofVScrrYrF0WHQxdcYMG6VstOCKe8AV2tjB+0YgMidG/rdkWstbWQIHnl
HEuW04YaxvISAWv0UbZQEY7Y2gVNUkJIu3ShlhQDC0ivjJQqWXbb6uCNOna2pa/1HT1XHf0BSjX0
UQErmx5bHDOUIRabmKVqYmOKjjdBU/6UctGrNOk5cSjLje3K8xEQDXa/ioqbcg70roGMuveUId5C
S6WQREtURlxohhb4Dk+8RzdMMz1jIMWOrR4WpLKlrkZhqyJYpvVCktfAtpHEVv3fQBWrHXYqZOO4
4sR+kaTuWy183slUIq29O4s2O6rhXo8qvjXkbJnP2zoEZrHDQFvLhqZxBcVKZY4yhnxFM90fktN1
x36WrRZLumxkyJ52lGRBitdMxgEMORmmXl0mq2gGM0FhooQQZwHFp1mwsQ6z9c6IxHywEXdM2Vqf
Oaiyvos39iNyzYzM1utkmZ5rlB3Kdc9KbQJUdzzq0wTvmaFLYKKoFgKe8YQrTkKuODHrwdZP/Rj5
rKKTlC4xDXFytiveZ3y3jbz1keMJ2FLgz3ZbJ15lDKrWIwPaTvFfyTBrX8Lht2VowbhSsYnweI44
30ZAoKlZqGZg/JanYVMUFHglH9oTMWdDuCCDre1RYwUwe3I2xXJZaJXpNkUvMzlZ5bga4TRUDdQS
pb6X7y3tTs1uE/IK2pxUtOn8vAbc5lT4EYlA4SXJcfndzL/eWkPEttpIWJKTDUgYxtdFvdC9+6KN
cD9akrMpdcra0Ku/lNg5EJgxKxP7X2v8YCF+teJMW04z/qvhShC+TVOXPTV1aQ6EuRqqibRUpljn
HXA23R/cllkvU8W5U+tJkK7XMeDxgyvgUQl2xNZUyOhQJdQrj6Q1n+NxSCA9+E5/7Ry7aQlNOiIJ
DyuRBO02WH2keW9LUKcS3ZTh4bjhmlGlwqVJr8wTLaLpVXlKoInkXDlFbqVOEO+E+AY6+So1B4nE
perOGSy3ZI0RtrY3mzxXH9W0rbmf1flbUmu/ErTza3fSnsslYXsn1+XkNIlzvwsnmzpG7JMjmNE1
4u3mTLTM9mIjRhoqoFKb64aeRW2YXfnwGCY+H5GRGYtXb3TMHB+MGvtZNZqV4DxaGktBZSS9w0Dt
7K7m66aDdjPUhnGkjYhMP5ptWwQk4l4nFRe0cnCHi3UhpbvPG9Fv3cG3utKh/B65TtGNDHrdo0Tm
HzSBe1vmpMKg0cCxMFJaycHbROMgmOFt6PGVwIDFUNHAx+Qwvn29Rji1UXUJ0U6LWa0fRzg/aXpO
i5HY3QRHzak5xdgR6xtXrlZKaWi1PY7udhw5qssILt5XgntyCNfzKOQ9OQ3E5Yl+Xmbtx9Y1OneM
KkhPA1ePyDzjeXnnI+XF41l55/AnyQpHwPTnRzRUjIhZY/O+mlC/SDLjOQDDR+cg4MpI1MTlmnxn
heWAJwm2f7co8B4oxDv44wom4T1myD15s8BjKENbPsT3338vd310Uo47Iwpz4N0Aq8gnOLudKsqm
ZsEFaOMStIxiuTJXEx5PQ9y9iCyfBrNVirtZOGOzLmHT2C5RbXe7toB+p/OHW32Q2gol6styesuC
zrKchpSZn+B/MnlWJ1aiDDmy3Okx768YDcql7lmlVCcVWtvlF2qHS/3DIpeaThOrPsdD2RbJjPK9
hSM99+vmf+n8P7qY4Y5xW8z1JQO2nP9/d3zPyP+7P8bz/+/ev3eT//dbfHrmfSSvzr3noHYf1OWA
h8JxPn8UYtyWNvLldNkh1jg8wai7dS2Ml9Pe2sMTx4n4XI6WMc89BND3vZTON5bQBsUdhbTt0Lpu
5vBEh1if0L5DrpzM9eA3SfI8wbMlnvm5H4HNXy3x8NID8erPfbwvywiJ8va+2jGR0XMkOJQQtu/c
4uF5tXzExQalS5CsTuONRWC6GLNZchnLx3Ibr4M/MLiYT/F6Ac0yvLcBN6rS/2MX/+T9CogALd3D
kEO6b10r5eCZExFBR5fTFQVv6+8G8sYnJyrqhjcVUOO4AqRvdPik/LpGMPsEZgdFTZd3ttZSn/4c
z3ldKj1dURYi3Vo75HTVT7RAtUSnYzbk1FV6lJ2HeB/NLnYcO9L/NODreRyNjU6qkqvQs8V3mtG+
2S0QgeKiK5AFgoJAPhnP6Yadrdf+aeDNfQDdX8598Mn1b28e+aeZPE9wq70ggXv3/DE/REFR3+nN
T6/1C/UV1InUSqlXseVEHKdBbuJaaCCCSvLE6mDkw/QBy9S8KZSU6VRVCBR90Aa2N+YL86aRrppR
6IZxvwixxqEfO8aVYLUXfQwryA7lfSgd9WZEApt2VzFfFXUCa9POW7f6n4Zpo+3VEoz3ANwCPwq1
gC44BTP2PR0u9V//RVBE831h2CpAASC3RCpvZsHmfarouJu8EUxvCxGRL7D4UHYZb62/JXjmYqC3
WSuErI9w6iaFwHsvxN1ylWNjK8NDn7suzT9LON7QLV49k4Iv7cHwwo9WwUCq2IFI6alx01ZZx+eg
VFDO8bioo7WcttqXtJ6LaNU3P6YZ4CdsC0qfsmmoGAajkNGisgPDaMBomU96HcbrggGVc6t5uLZ4
Sxy3+UE3NBBH+EgDy7GoYYjfZwM9aOEJlnQ8b+CK39dPBq2M8fvqxaCFN36fXgza2KPKNXEIWjWe
kc02uRRc4IbdOThQrTcIorXD9Rc8YvQDP8CCbUak7CvynYJ0gETT4DstFK6Ov1tbB2Le5x/tOkej
7pZL7dQwW+HxVne9kxxxKh8B6qBvWw0KJ4dchFR5SG0VTMVBuHHEbRuRvbF7TFZeWtexmbNCaHPq
56Yx2hyiWxCHEXS0+RDqjxvqtnilmW63fZTPxl3KIlweVf3RMBs7RrzmPu3LkRUocksYw6tklizT
B8j26PolrWFbt6B/3xeY+1+IuT+uoLcxSEbPH9d7AHQR2yKJ/ZlnSqq1BFWm5aigpez+oOzSmOXG
WG4geULkbx8NK3dKOEZDY9ZC46HiRWlE9Ef8u21UzMZd/JR/SzdlHT/l7sac8QvO+OO+ZMugg32m
o8Be4PlpRoGmoM+aZhThywPoknPzAuri0kW+e7bOfB2eqFFanithDfAUKeFznqkNs4G0TLpD46pb
9Aw2azLtMGM7ZHNbXGFc7+6Q39nQnhUdkC5KU3yg9ALb/23DBEqfvjBawNpWfnxNwQP8VaeOkmmO
MF+FLa/+/Mi4phpvG6dr1fAxcqrxEgyNpLppe92LMCoAOqH7ibG0QpDGjeql3jw033FVpBzxDbDy
6ZZyHydGyOj8LE1Wp3jYnKGGVBZLWrrZ5P+zRmhVNYSk8uELXhv0uDjLUqoWWx2bNqoBS8dQ0Fy6
VFUx/3ekX60KVYTgLE3cUK9Uc4VmFQhIIZn6+fQM3gSfpwHn9AtcGEuDeAZ+OYZYF2KujQGV9nRZ
j940SsthR1ExpabR7lvispGc+F8mJAVD1pGBkl/yLxMAzX66PrnsWaDpMD0F9h3wQntRucpe+h7C
eZEHtvyEL5HHy+qFvuPmwy1GCldPtNhw9EDBPZFkWi1LBT6oErowBl2h7C15u0Y55lygz+936GJ7
XErB5YRpgd/u7m5tz2u6r77sN9KB1My9MFNGTkz1vNKgXKXdEy46ri1aYKbuHKGOGr3tY1NDAoLC
09DavtK4/i3JsYdS9UShe+zYALS/05IYwOYvmRkuI266K/epM7JBaYYbDQS2sFoC/D42Ct/MJnGW
JQX/1qBNLCqygcOltTI6ojXMPLGfjmmx1JYYLsDAP4iquLhWaJ0X31SU0n7t7olTTqimHteln0Ax
O+FQpUHFJed+mra1y2dry0FB+6DhlC0zl3dOSqU5hHdzOTfl1yhRLYE94Y6oq6G7Ml+tdKBkzdcL
9qnSzkmsLK28a1nWORSosvRybr42e1EJAJo44TtFPXtEMM7KZXNStSb4/FRY8ygWl6qAWHaGhWwK
ynk6KNnvqlhouVB2QRiGgYxTWXqnGas+gMfvSutrNN3USS5R99YbO3V2KB53VdtaW+AAe9KZ8I/L
A5+D/I30NwHUcaHCBkx9fDxYjxuTwZoM8cZchoyvUQgGZz+n1YgV+oF06jYnoezsyPrVYEgTl9rt
K5WYt0RqeeKjSlM8IwTlNCdOreESHU6odWNZ4bOBpo3yukMyBE1rte3AtXViMzyv9ZExYGE7u1/P
Nda2E6YjixX4WpNgmiwCaUFx46UP09bc6RMrcDXedG20pd6VtiMfgXmouHl4eFUQS6k+x/GFn4Z+
XExfugTrimwrc3lECiZdc1Af0qLlBvxhlafXJ3rviTqMviWnSEiV4zsPGKq+eqXcsB0dcwRFD0+K
SJm1VlsfJ+MmN0qmUafYW0JoH21vyR+/0rKFP9slqwa/ermqVuiVRKwulGRwwhH1cpCbfTZ1EFyF
jRyJxmx8jDhxzpu9N62MqgpX82UJUq6zetkxfnq6/CPZ/tAqbZyyZ6asa6M1FA3RBRlcsNHO+J4W
sxGM8KqY2paLIkY4UOPLm9Zrw5CuLnpEMoNHm3ZJ9mgtOuJ1DF0IUZQrAo7ygaZRVQI+8aBO5HiR
xCDmcTgN86v16LOAml7JslW2K5jv0UGxfo+VEWqwgwUB1d2KzSBNmqxBcm+s7xMuRWzXBaTO+KHb
G3EBoaRPa1CYb4f8DUm8Xj//BZTmKzFbJEBtzqRTdfAyFBAbSiyNLv0rDIkWdmE9fsBoUlyl1WtA
F1vFm2J5vC4pt8QOz+ewWAtj0yqNQZFLDgPYoDZz+3WtbW9L2xJRXnDxp3hIDJvX+mUeuzeGUV0f
cVFnVJvo1NWc6n6WermmkaRO/p8yj/XE66yuDSAajj1zUk07vlUZoTd0IxR/0zRiVauSo1qjAwlw
Lm7r7NokKJNekoAVBZ0tMmVdyfKvHAkaGfsbiVNHu48wqtnqevZWN6vz3iUezrc/mNGHhklery5U
pCEOHasxa08DZQygeSp4PW5ueRX+d+frFovl1+H0WqMWZzPGF0GaB7N1vTWlnfnvdFAz6VY3umXL
YBrCdFmmFlymuUrM6EoAvLYqCnI0UXZ+hEmKL++/bsbsVnHuV6ean66l14b+fLW+uzRnHQo01//k
2uhWsYhgMf/VOyX/PT96/y+L31e5AaR5/+/e/v7d+8X+3we4/3d/f3z3Zv/vb/F5ESzAn/B4IDoQ
Tw/fHWJSRe/x0U/HL0mb3wT+jIKB/uwRPfiZ9q0f8P+Pekdg6i0omGidn8E8dxbO5wGGEukU2Sev
34MxCy/CKDjFwxsvgohOoaWFGZgipwFdSJrE0ZXIL5OehFlUcWL3drUM0oswS3CZpPjBmL7PaPUE
/7Pw1DAxNQWjvxzslXf56lZ2drgdjtu+TOIldCaI8wPj+yO00Rz0nVwJX8T6DYWRZd3XaZIHtNP1
wPherosVmDBo9WUhcREmEacF7uxgH2x81VIXPpWwKGZ9YPXsGTxqzRCweOh8V9DNfl1ByXx5fLg/
VotORcG5xMhO4BHLuTf18aI8udpeQB0WJaTXdGCjbBRYJDOAUBSw8TYTe2wS0akdQCRxGsRBWozJ
1KtedVeA4ZfjTypWiIyLPtwKn6VOoMFb49M6VtgHHfvmdDkqgcsXPWGvOhXO3GmQezNG5alcXgOv
SmVr4vk9/asgH4gzgBiBW7nUcqIZIpc+NPl8OYQfiMPZLDUpW1oXsXiET+x0/kc9fafyu+ePQdXp
ZuUsR92gPk9XaaoUBYxFCgLP4mnmURhLfQZAxSBDT7h4HywKnQySJYtgksyuxCUtK+SJJAGYmiQL
1C3Nv/zyCx6UgscKYxzMSFgEwuos10dU2rG6aGAko2Z8En6cB2m6Wuby3WGOnSbtJ8MoOSvXJeVS
pAgXi2AW+ngd5K44lq+BgxKI8YE6lIc70+m3CRpQx7rJf7Ak2stN5YVh6gUd2J/g0d9EvmmKW6tV
xolcwXxENxm3fMST27dlDzPRWFJ2bPs0Ae7QmtY27mmB7gUxsCKYrnI83GZHlFMRC/GnWoIvDY9P
VdYidQhtpVr5/FePsr/fj/b/3hwdPn1x9FXaaPH/9u6OR9r/e4DlRuPRjf/323x6OIBNz4LpufAn
oEX+NL+D4wlOBHbFz2Cm8dIwP74CwxWf8lEYs3AZ+VfyInqYnfamZ37IuzFprR3HQY8vSRf9CBNd
KcAx2MVZqFgEeMB35l+Bo3iMhhL8JdBzD4ev3Up9sJbvX75+8+qvR093e71vv/32Zz+NARP4Rv6M
nB83YAAQnhy/efL++eEbdjdh/EuiKLkEKDTb/YnHkt3HV3lwYypuPjefm8/N5+Zz87n53HxuPjef
m8/N5+Zz87n53HxuPjefm8+/zef/ARhdjSgAQAEA
--g4AlWPTQws--
How-To-Repeat:
Fix:
Modified the status to properly check for circularities.
----------------
(eval-when (eval compile load)
(fmakunbound 'get-judgement-tcc))
(defvar *possible-judgements* nil)
(defun pc-complete (decl)
(let* ((*dependings* nil)
(*proved-dependings* nil)
(*unproved-dependings* nil)
(*defn-dependings* nil)
(*axiom-dependings* nil)
(*assumption-dependings* nil)
(*depending-chain* nil)
(*depending-cycles* nil)
(*in-checker* nil)
(*current-context* (context decl))
(*possible-judgements* (possible-judgements decl))
(fdecls (union (union (refers-to decl)
(proof-refers-to decl))
(assuming-tccs decl)))
(decls (union fdecls *possible-judgements*)))
(pc-analyze* decls)
(mapc #'(lambda (y)
(cond ((typep y 'formula-decl)
(if (axiom? y)
(push y *axiom-dependings*)
(if (assumption? y)
(push y *assumption-dependings*)
(if (proved? y)
(push y *proved-dependings*)
(push y *unproved-dependings*)))))
((and (or (typep y 'const-decl)
(typep y 'def-decl))
(definition y))
(push y *defn-dependings*))))
*dependings*)
(cond (*depending-cycles* "circular")
((and (null *unproved-dependings*)
(proved? decl))
"complete")
(t "incomplete"))))
(defmethod pc-analyze ((decl formula-decl))
(let* ((*dependings* nil)
(*proved-dependings* nil)
(*unproved-dependings* nil)
(*defn-dependings* nil)
(*axiom-dependings* nil)
(*assumption-dependings* nil)
(*depending-chain* nil)
(*depending-cycles* nil)
(*current-context* (context decl))
(*possible-judgements* (possible-judgements decl))
(fdecls (union (union (refers-to decl)
(proof-refers-to decl))
(assuming-tccs decl)))
(decls (union fdecls *possible-judgements*)))
(pc-analyze* decls)
(mapc #'(lambda (y)
(cond ((typep y 'formula-decl)
(if (axiom? y)
(push y *axiom-dependings*)
(if (assumption? y)
(push y *assumption-dependings*)
(if (proved? y)
(push y *proved-dependings*)
(push y *unproved-dependings*)))))
((and (or (typep y 'const-decl)
(typep y 'def-decl))
(definition y))
(push y *defn-dependings*))
(t)))
*dependings*)
(if (axiom? decl)
(format t "~%~a.~a is an axiom." (id (module decl)) (id decl))
(if (proved? decl)
(format t "~%~a.~a has been PROVED." (id (module decl)) (id decl))
(format t "~%~a.~a is UNPROVED." (id (module decl)) (id decl))))
(when *depending-cycles*
(format t "~%~%***Warning***: The proof chain for ~a is CIRCULAR in the following:"
(id decl))
(loop for x in *depending-cycles*
do (format t "~% ~a.~a" (id (module x))(id x))))
(cond
((and (null *unproved-dependings*) (proved? decl))
(format t "~%~% The proof chain for ~a is COMPLETE." (id decl)))
((proved? decl)
(format t "~%~% The proof chain for ~a is INCOMPLETE.~
~% It depends on the following unproved conjectures:"
(id decl))
(loop for x in (pc-sort *unproved-dependings*)
do
(format t "~% ~a.~a" (id (module x)) (id x)))))
(when *proved-dependings*
(format t "~%~% ~a depends on the following proved theorems:"
(id decl))
(loop for x in (pc-sort *proved-dependings*)
do
(format t "~% ~a.~a" (id (module x)) (id x))))
(when *axiom-dependings*
(format t "~%~% ~a depends on the following axioms:"
(id decl))
(loop for x in (pc-sort *axiom-dependings*)
do
(format t "~% ~a.~a" (id (module x)) (id x))))
(when *defn-dependings*
(format t "~%~% ~a depends on the following definitions:"
(id decl))
(loop for x in (pc-sort *defn-dependings*)
do
(format t "~% ~a.~a" (id (module x)) (id x))))
(when *assumption-dependings*
(format t "~%~% ~a depends on the following assumptions:"
(id decl))
(loop for x in (pc-sort *assumption-dependings*)
do
(format t "~% ~a.~a" (id (module x)) (id x))))
(when *possible-judgements*
(format t "~%~% ~a may depend on the following judgements:"
(id decl))
(loop for x in (pc-sort *possible-judgements*)
do
(format t "~% ~a.~a" (id (module x)) (id x))))))
(defun possible-judgements (decl)
;;; We collect all judgements of the current context that might be
;;; involved in the proof of the decl. This includes all subtype and
;;; number judgements, as well as any name or application judgements
;;; whose decl is in decls.
;;; [owre - 2005-09-11] Now just collect subtype judgements.
(let ((jtccs nil))
(dolist (jdecl (if (from-prelude? decl)
(judgement-declarations
(judgements (context decl)))
(remove-if #'from-prelude?
(judgement-declarations
(judgements (context decl))))))
(let ((tcc (get-judgement-tcc jdecl decl)))
(when tcc (push tcc jtccs))))
;; (do-all-declarations #'(lambda (decl)
;; (let ((tcc (get-judgement-tcc decl decls)))
;; (when tcc (push tcc jtccs)))))
jtccs))
(defmethod get-judgement-tcc ((jdecl subtype-judgement) decl)
;; This one is difficult, since it is not obvious when the judgement comes
;; into play. Just collect them all.
(if (generated-by jdecl)
(get-judgement-tcc (generated-by jdecl) decl)
(find-if #'judgement-tcc? (generated jdecl))))
(defmethod get-judgement-tcc ((jdecl number-judgement) decl)
;; Similarly, don't really know when a number-judgement kicked in.
;; (if (generated-by jdecl)
;; (get-judgement-tcc (generated-by jdecl) decls)
;; (find-if #'judgement-tcc? (generated jdecl)))
)
(defmethod get-judgement-tcc ((jdecl name-judgement) decl)
;; Ignore it, if the associated declaration is not in decls
;; (when (memq (declaration (name jdecl)) decls)
;; (if (generated-by jdecl)
;; (get-judgement-tcc (generated-by jdecl) decls)
;; (when (memq (declaration (name jdecl)) decls)
;; (find-if #'judgement-tcc? (generated jdecl)))))
)
(defmethod get-judgement-tcc ((jdecl application-judgement) decl)
;; (when (memq (declaration (name jdecl)) decls)
;; (if (generated-by jdecl)
;; (get-judgement-tcc (generated-by jdecl) decls)
;; (find-if #'judgement-tcc? (generated jdecl))))
)
(defmethod get-judgement-tcc ((jtcc judgement-tcc) decl)
(get-judgement-tcc (generated-by jtcc) decl))
(defmethod get-judgement-tcc (decl fdecl)
(declare (ignore decl fdecl))
nil)
(defmethod pc-analyze* ((fdecl formula-decl))
(let ((*depending-chain* *depending-chain*))
(cond ((and (not (judgement-tcc? fdecl))
(memq fdecl *depending-chain*))
(pushnew fdecl *depending-cycles*)
*dependings*)
((memq fdecl *dependings*)
*dependings*)
(t (push fdecl *dependings*)
(push fdecl *depending-chain*)
(cond ((from-prelude? fdecl)
*dependings*)
((or (axiom? fdecl)
(assumption? fdecl))
;; No need to include proof-refers-to in this case
(let ((decls (union (refers-to fdecl)
(remove-if-not #'tcc?
(generated fdecl)))))
(pc-analyze* (union decls (possible-judgements fdecl)))))
(t (let ((decls (union (union (refers-to fdecl)
(proof-refers-to fdecl))
(remove-if-not #'tcc?
(generated fdecl)))))
(pc-analyze* (union decls (possible-judgements fdecl))))))))))