At: normalization lemma 1 1 1 1 1 1 1 5 1 1 1
1. hyp: Formula List
2. concl: Formula List
3. 
f
hyp.(
(f) > 0)
4. M: Formula List
5. N: Formula List
6. f: Formula
7. y1: Formula
8. y2: Formula
9. (y1
y2) > 0
10. hyp = (M @ (y1y2.N))
11. ( < M @ N,y1.concl > ) < ( < M @ (y1y2.N),concl > )
(L:Sequent List.
sL.((s) = 0)
& (sL.|= s |= < M @ N,y1.concl > )
& (a:Assignment. sL.a |
s a | < M @ N,y1.concl > ))
( < y2.(M @ N),concl > ) < ( < M @ (y1y2.N),concl > )
By:
SequentRankReduce 0
THEN
GenConclOnAps
Generated subgoals:None
About:
