Nuprl - Pf assignment_monotone 1 1 5 1 1 1

PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

1. f: Formula
2. y1: Formula
3. y2: Formula
4. a: Assignment
5. a': Assignment
6. a' extends a
7. a |= y1 a' |= y1
8. a | y1 a' | y1
9. a |= y2 a' |= y2
10. a | y2 a' | y2
11. a |= y1y2

a' |= y1y2

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

Generated subgoals:

1 12. a | y1
a' | y1 a' |= y2

2 12. a |= y2
a' | y1 a' |= y2

About:

1	12. `a \| y1` `a' \| y1 a' \|= y2`
2	12. `a \|= y2` `a' \| y1 a' \|= y2`