PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: formula imp falsifiable lemma 1 1 1 1 1 1 1
1. a: Assignment
2. q: Formula
3. r: Formula
4. n:
5. (q under a) = n
6. m:
7. (r under a) = m
8. n m = 3

n = 3
By:
ThreeInd -5
THEN
ThreeInd -3
THEN
AbReduce -1
Generated subgoals:

14. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
24. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
34. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
44. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
54. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
64. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
74. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
84. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3
94. (q under a) = 3
5. (r under a) = 3
6. 3 = 3
3 = 3

About:
equal