PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: assignment monotone 1 1 2 1
1. f: Formula
2. x: Formula
3. a,a':Assignment. a' extends a (a |= x a' |= x ) & (a | x a' | x)
4. a: Assignment
5. a': Assignment
6. a' extends a

(a |= x a' |= x ) & (a | x a' | x)
By:
With a (Analyze -4)
THEN
With a' (Analyze -1)
THEN
Analyze -1
THEN
Analyze -1
Generated subgoal:

13. a: Assignment
4. a': Assignment
5. a' extends a
6. a |= x a' |= x
7. a | x a' | x
(a |= x a' |= x ) & (a | x a' | x)

About:
andimpliesall