PROOF EDITOR
Symbol
Next action
Add assumption
Add proof line
Create goal
Edit goal
Delete proof line
Delete goal
Proof complete
Adding proof line 4.
Edit which goal?
A
ANDI
ANDE
ORI
ORE
IMPI
IMPE
NOTI
NOTE
RAA
NOTNOTE
ALLI
ALLE
SOMEI
SOMEE
=I
=E
ALLI
R
ALLE
R
SOMEI
R
SOMEE
R
Assumptions
Formula
Source lines
Rule used
CANCEL
Premise:
Conclusion:
Error message appears here.
Choose from the menu how you want to proceed:
--- select ---
Edit line section
Restart line
Abandon current action
Help