thus
( (p . {}) `2 = 7 implies ex r being Nat 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] & r = (((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 ex b1 being Nat st b1 = 0 )proof
A1:
{} ^ <*0*> = <*0*>
by FINSEQ_1:34;
A2:
{} ^ <*1*> = <*1*>
by FINSEQ_1:34;
reconsider v =
{} as
Element of
dom p by TREES_1:22;
assume
(p . {}) `2 = 7
;
ex r being Nat 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] & r = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
then consider w,
u being
Element of
dom p,
T,
X,
Y being
FinSequence of
s,
y,
z being
type of
s such that A3:
w = v ^ <*0*>
and A4:
u = v ^ <*1*>
and A5:
(p . v) `1 = [((X ^ T) ^ Y),z]
and A6:
(p . w) `1 = [T,y]
and A7:
(p . u) `1 = [((X ^ <*y*>) ^ Y),z]
by Th10;
reconsider a =
Sum ((size_w.r.t. s) * ((X ^ T) ^ Y)) as
Nat by Lm1;
reconsider tt =
(((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a as
Nat ;
take
tt
;
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] & tt = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
thus
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] &
tt = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
by A1, A2, A3, A4, A5, A6, A7;
verum
end;
thus
( not (p . {}) `2 = 7 implies ex b1 being Nat st b1 = 0 )
; verum