Nuprl - Pf formula_valid_iff_sequent

PrintForm Definitions sequent valid Sections ClassicalProps(jlc) Doc

At: formula valid iff sequent valid 1 1 2 1 1 1

1. F: Formula
2. a:Full(F). a |= F
3. a: Assignment
4. True
5. a | F
6. True

a |= < nil,[F] >

By: Witness2 a

Generated subgoals:

1 2. a: Assignment
3. True
4. a | F
5. True
a Full(F)

2 2. a: Assignment
3. True
4. a | F
5. True
6. a |= F
a |= < nil,[F] >

About:

1	2. `a:` `Assignment` 3. `True` 4. `a \| F` 5. `True` `a Full(F)`
2	2. `a:` `Assignment` 3. `True` 4. `a \| F` 5. `True` 6. `a \|= F` `a \|= < nil,[F] >`