Nuprl - Pf assignment_monotone 1 1 4 1 1 1 1

PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

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' |= x1 a' |= x2

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

Generated subgoals:

1 12. a |= x1
a' |= x1 a' |= x2

2 12. a |= x2
a' |= x1 a' |= x2

About:

1	12. `a \|= x1` `a' \|= x1 a' \|= x2`
2	12. `a \|= x2` `a' \|= x1 a' \|= x2`