Nuprl - Pf formula_and_sat

PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

a:Assignment, q,r:Formula. a |= qr a |= q & a |= r

By: UnivCD THEN Analyze 0 THEN Unfolds [`formula_sat`;`formula_falsifiable`] 0 THEN Reduce 0

Generated subgoals:

1 1. a: Assignment
2. q: Formula
3. r: Formula
(q under a) (r under a) = 3 (q under a) = 3 & (r under a) = 3

2 1. a: Assignment
2. q: Formula
3. r: Formula
((q under a) (r under a) = 3) ((q under a) = 3 & (r under a) = 3)

About:

1	1. `a:` `Assignment` 2. `q:` `Formula` 3. `r:` `Formula` `(q under a) (r under a) = 3 (q under a) = 3 & (r under a) = 3`
2	1. `a:` `Assignment` 2. `q:` `Formula` 3. `r:` `Formula` `((q under a) (r under a) = 3) ((q under a) = 3 & (r under a) = 3)`