Nuprl - Pf assignment_monotone 1 1 1

PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

1. f: Formula
2. x: Var

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

By: UnivCD THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 3. a: Assignment
4. a': Assignment
5. a' extends a
6. a |= x
a' |= x

2 3. a: Assignment
4. a': Assignment
5. a' extends a
6. a | x
a' | x

About:

1	3. `a:` `Assignment` 4. `a':` `Assignment` 5. `a' extends a` 6. `a \|= x` `a' \|= x`
2	3. `a:` `Assignment` 4. `a':` `Assignment` 5. `a' extends a` 6. `a \| x` `a' \| x`