Page 733 of 800
| Page 733 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Infer-seqop used on non-meta term: x
The Infer sequent operator applied to a sequent 
and a metaterm h yields 
. Thus, the Infer operator allows to move a hypothesis h from the set of premisses to the conclusion. The Infer operator can be used for hypothetical reasoning like 'Assume the axioms of Peano arithmetic, prove some lemma, conclude that the axioms of Peano arithmetic infer the lemma'. In this case the axioms of Peano arithmetic serve as hypothesis h.
The 'Infer-seqop used on non-meta term' indicates that the hypothesis h was illformed. The error may indicate an error in the proof or a bug in a tactic.
| Page 733 of 800 | Search logiweb.eu |