:: deftheorem defines cutdeg PRELAMB:def 15 :
for s being non empty typealg
for p being Proof of s
for b₃ being Nat holds
( ( (p . {}) `2 = 7 implies ( b<sub>3</sub> = cutdeg p iff ex T, X, Y being FinSequence of s ex y, z being type of s st
( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b₃ = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) ) & ( not (p . {}) `2 = 7 implies ( b₃ = cutdeg p iff b₃ = 0 ) ) );