Page 737 of 800
| Page 737 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
All-seqop catches variable x which is free in the following condition: c
The All sequent operator applied to a sequent 
and a metavariable 
yields 
provided does not occur free in any premise or side condition. The 'All-seqop catches variable which is free in condition c' indicates that occurs free in c.
Users typically read proofs start to end whereas the sequent evaluator typically evaluates proofs end to start. The 'All-seqop catches variable which is free in condition' typically occurs when a proof first assumes that a metavariable satisfies some side condition and then assumes the metavariable to be arbitrary. The All operator can implement the assumption that a metavariable is arbitrary whereas the Endorse operator can implement an assumption that a metavariable satisfies some side condition.
| Page 737 of 800 | Search logiweb.eu |