Nuprl - Pf formula_and_sat

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

a |= q & a |= r

By: FwdThru Thm* x,y:. x y = 3 x = 3 & y = 3 [-1] THEN Sel 2 (FwdThru Thm* x,y:. x y = 3 x = 3 & y = 3 [-2]) THEN OnHyps [-2;-1] (Fold `formula_sat`)

Generated subgoal:

1 5. a |= q
6. a |= r
a |= q & a |= r

About: