Nuprl - Pf normalization_lemma 1 1 1 2 1 1

PrintForm Definitions normalization Sections ClassicalProps(jlc) Doc

1. hyp: Formula List
2. concl: Formula List
3. S:Sequent. (S) < ( < hyp,concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
4. fconcl.((f) > 0)
5. M: Formula List
6. N: Formula List
7. f: Formula
8. (f) > 0
9. concl = (M @ (f.N))

L:Sequent List. sL.((s) = 0) & (sL.|= s |= < hyp,concl > ) & (a:Assignment. sL.a | s a | < hyp,concl > )

By: MoveToEnd 3 THEN OnHyps [-1;0] (i.HypSubst -2 i)

Generated subgoal:

1 3. fconcl.((f) > 0)
4. M: Formula List
5. N: Formula List
6. f: Formula
7. (f) > 0
8. concl = (M @ (f.N))
9. S:Sequent. (S) < ( < hyp,M @ (f.N) > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < hyp,M @ (f.N) > ) & (a:Assignment. sL.a | s a | < hyp,M @ (f.N) > )

About: