Nuprl - Pf formula_and_falsifiable

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 Rewrite (HigherC valuation_unrollC) 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)`