PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: assignment monotone 1 1 3 1 1 2
1. f: Formula
2. x1: Formula
3. x2: Formula
4. a: Assignment
5. a': Assignment
6. a' extends a
7. a |= x1 a' |= x1
8. a | x1 a' | x1
9. a |= x2 a' |= x2
10. a | x2 a' | x2
11. a | x1x2

a' | x1x2
By:
FwdThru Thm* a:Assignment, q,r:Formula. a | qr a | q a | r [-1]
THEN
Analyze -1
Generated subgoals:

112. a | x1
a' | x1x2
212. a | x2
a' | x1x2

About:
implies