gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

CS-PRE-LEFT-HMEQ-LEFT-REDUCTION test fails. #107

Open gheber opened 8 years ago

gheber commented 8 years ago

CS-PRE-LEFT-HMEQ-LEFT-REDUCTION []:

(CAT:CMBN-? (EVAL PHI) (IF (MEMBER PHI (QUOTE (CAT:BDD CAT:DG-GD CAT:ID-FG CAT:DG-GD CAT:HG))) CAT:BC CAT:TC))

evaluated to

----------------------------------------------------------------------{CMBN 11}
<1 * <TnPr <TnPr <<GBar<- (3)><- NIL>>> (4 5 6)> <<Abar[3 (9 -8)][3 (1 0)]>>>>
------------------------------------------------------------------------------

which does not satisfy

CAT:CMBN-ZERO-P

.