PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
falsifiable
lemma
1
1
2
1
1
1
1
2
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
4.
(q under a) = 3
5.
(r under a) = 3
6.
3
= 3
7.
case 3
: 3
0; 3
1; 3
2; = case 3
: 3
0; 3
1; 3
2;
3
= 3
By:
AbReduce -1
Generated subgoal:
1
7.
2 = 0
3
= 3
About:
= 3: 3 
0; 3
1; 3 2; = case 3: 3 0; 3 1; 3 2;
3 = 3
