thus
( (p . {} ) `2 = 7 implies ex r being Nat ex T, X, Y being FinSequence of the carrier 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:47;
A2:
{} ^ <*1*> = <*1*>
by FINSEQ_1:47;
reconsider v =
{} as
Element of
dom p by TREES_1:47;
assume
(p . {} ) `2 = 7
;
ex r being Nat ex T, X, Y being FinSequence of the carrier 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 the
carrier 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 Lm3;
take
(((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a
;
ex T, X, Y being FinSequence of the carrier 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] & (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((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 the
carrier 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] &
(((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((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