Page 732 of 800
| Page 732 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
At-seqop used on non-quantifier: R
The At sequent operator applied to a sequent 
and a metaterm y yields 
where B is the result of replacing 
by y in A. The 'At-seqop used on non-quantifier' indicates that the conclusion of the sequent did not have form 
. The error may indicate an error in the proof or a bug in a tactic.
| Page 732 of 800 | Search logiweb.eu |