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
ALLIR
ALLER
SOMEIR
SOMEER
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