k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S
n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S
n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).