PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: assignment monotone 1 1 3

1. f: Formula
2. x1: Formula
3. x2: Formula
4. a,a':Assignment. a' extends a (a |= x1 a' |= x1 ) & (a | x1 a' | x1)
5. a,a':Assignment. a' extends a (a |= x2 a' |= x2 ) & (a | x2 a' | x2)

a,a':Assignment. a' extends a (a |= x1x2 a' |= x1x2 ) & (a | x1x2 a' | x1x2)

By: UnivCD

Generated subgoal:

16. a: Assignment
7. a': Assignment
8. a' extends a
(a |= x1x2 a' |= x1x2 ) & (a | x1x2 a' | x1x2)


About:
allimpliesand