chapter  7
The Midsequent Theorem
Pages 10

N o w b a 1 <— » 3 z ( z e t A w ) fo r a n ew v a r ia b le z , an d so G p ro v e s a ^ <— » 3 z ( z e t A w ) 0 , i .e .

G b a^0 <— > 3 z ( ( z e t ) * A w 0 ) .

I s h a ll show th a t

(9 b ) G b a 0a -> 3 z ( ( z e t ) * A w 0 ) ,

w hence a lso ( 9 a ) . In o rd e r to see ( 9 b ) , i t su ffices to p ro v e

(9 c ) G b V x w 0 3 z ( ( z e t ) * A w 0 ) ,

an d th is c e r ta in ly h o ld s i f t is a v a r ia b le . I f t — g ( / / ) an d d e f ( / / ) = m th e n b y in d u c tiv e h y p o th e s is fo r e v e ry i < m

G b V x w 0 3 t? ( i) ( ( t f ( i ) = /< ( i ) ) * a w 0 ) , G b V x w 0 -> A < 3 t f ( i ) ( ( t f ( i ) s / * ( i ) ) * A w 0 ) | i < m > .