Page 736 of 800
| Page 736 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
All-seqop catches variable x which is free in the following premise: p
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 premise p' indicates that occurs free in p.
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 premise' typically occurs when a proof first assumes that a metavariable satisfies some statement and then assumes the metavariable to be arbitrary. The All operator can implement the assumption that a metavariable is arbitrary whereas the Infer operator can implement an assumption that a metavariable satisfies some statement.
| Page 736 of 800 | Search logiweb.eu |