Nuprl - Pf normalization_lemma 1 1 1 1 1 1 1

PrintForm Definitions normalization Sections ClassicalProps(jlc) Doc

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

L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (f.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (f.N),concl > )

By: FormulaCases -4

Generated subgoals:

1 7. x: Var
8. (x) > 0
9. hyp = (M @ (x.N))
10. S:Sequent. (S) < ( < M @ (x.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (x.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (x.N),concl > )

2 7. x: Formula
8. (x) > 0
9. hyp = (M @ (x.N))
10. S:Sequent. (S) < ( < M @ (x.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (x.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (x.N),concl > )

3 7. x1: Formula
8. x2: Formula
9. (x1x2) > 0
10. hyp = (M @ (x1x2.N))
11. S:Sequent. (S) < ( < M @ (x1x2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (x1x2.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (x1x2.N),concl > )

4 7. x1: Formula
8. x2: Formula
9. (x1x2) > 0
10. hyp = (M @ (x1x2.N))
11. S:Sequent. (S) < ( < M @ (x1x2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (x1x2.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (x1x2.N),concl > )

5 7. y1: Formula
8. y2: Formula
9. (y1y2) > 0
10. hyp = (M @ (y1y2.N))
11. S:Sequent. (S) < ( < M @ (y1y2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= < M @ (y1y2.N),concl > ) & (a:Assignment. sL.a | s a | < M @ (y1y2.N),concl > )

About:

1	7. `x:` `Var` 8. `(x) > 0` 9. `hyp = (M @ (x.N))` 10. `S:Sequent. (S) < ( < M @ (x.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= S ) & (a:Assignment. sL.a \| s a \| S))` `L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= < M @ (x.N),concl > ) & (a:Assignment. sL.a \| s a \| < M @ (x.N),concl > )`
2	7. `x:` `Formula` 8. `(x) > 0` 9. `hyp = (M @ (x.N))` 10. `S:Sequent. (S) < ( < M @ (x.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= S ) & (a:Assignment. sL.a \| s a \| S))` `L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= < M @ (x.N),concl > ) & (a:Assignment. sL.a \| s a \| < M @ (x.N),concl > )`
3	7. `x1:` `Formula` 8. `x2:` `Formula` 9. `(x1x2) > 0` 10. `hyp = (M @ (x1x2.N))` 11. `S:Sequent. (S) < ( < M @ (x1x2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= S ) & (a:Assignment. sL.a \| s a \| S))` `L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= < M @ (x1x2.N),concl > ) & (a:Assignment. sL.a \| s a \| < M @ (x1x2.N),concl > )`
4	7. `x1:` `Formula` 8. `x2:` `Formula` 9. `(x1x2) > 0` 10. `hyp = (M @ (x1x2.N))` 11. `S:Sequent. (S) < ( < M @ (x1x2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= S ) & (a:Assignment. sL.a \| s a \| S))` `L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= < M @ (x1x2.N),concl > ) & (a:Assignment. sL.a \| s a \| < M @ (x1x2.N),concl > )`
5	7. `y1:` `Formula` 8. `y2:` `Formula` 9. `(y1y2) > 0` 10. `hyp = (M @ (y1y2.N))` 11. `S:Sequent. (S) < ( < M @ (y1y2.N),concl > ) (L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= S ) & (a:Assignment. sL.a \| s a \| S))` `L:Sequent List. sL.((s) = 0) & (sL.\|= s \|= < M @ (y1y2.N),concl > ) & (a:Assignment. sL.a \| s a \| < M @ (y1y2.N),concl > )`