let p be non empty Tree-yielding FinSequence; Leaves (tree p) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
set i0 = the Element of dom p;
reconsider d0 = p . the Element of dom p as Tree by TREES_3:22;
consider j being Nat such that
A0:
the Element of dom p = 1 + j
by NAT_1:10, FINSEQ_3:25;
the Element of dom p <= len p
by FINSEQ_3:25;
then A3:
( j < len p & <*> NAT in d0 )
by A0, NAT_1:13, TREES_1:22;
A2:
<*j*> ^ {} in tree p
by A0, A3, TREES_3:def 15;
thus
Leaves (tree p) c= { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
XBOOLE_0:def 10 { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } c= Leaves (tree p)proof
let a be
object ;
TARSKI:def 3 ( not a in Leaves (tree p) or a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } )
reconsider x =
a as
set by TARSKI:1;
assume A1:
a in Leaves (tree p)
;
a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
then reconsider x =
a as
Element of
tree p ;
per cases
( x = {} or ex i being Nat ex q being FinSequence st
( i < len p & q in p . (i + 1) & x = <*i*> ^ q ) )
by TREES_3:def 15;
suppose
ex
i being
Nat ex
q being
FinSequence st
(
i < len p &
q in p . (i + 1) &
x = <*i*> ^ q )
;
a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } then consider i being
Nat,
q being
FinSequence such that A2:
(
i < len p &
q in p . (i + 1) &
x = <*i*> ^ q )
;
( 1
<= i + 1 &
i + 1
<= len p )
by A2, NAT_1:11, NAT_1:13;
then AB:
(
i + 1
in dom p &
p is
Tree-yielding )
by FINSEQ_3:25;
then
(
p . (i + 1) in rng p &
rng p is
constituted-Trees )
by FUNCT_1:def 3, TREES_3:def 9;
then reconsider p1 =
p . (i + 1) as
Tree ;
reconsider q0 =
q as
Element of
p1 by A2;
now not q0 nin Leaves p1assume AA:
q0 nin Leaves p1
;
contradictionconsider r being
FinSequence of
NAT such that A3:
(
r in p1 &
q0 is_a_proper_prefix_of r )
by AA, TREES_1:def 5;
consider w being
FinSequence such that A5:
r = q ^ w
by A3, XBOOLE_0:def 8, TREES_1:1;
<*i*> ^ r = (<*i*> ^ q) ^ w
by A5, FINSEQ_1:32;
then
(
<*i*> ^ q is_a_prefix_of <*i*> ^ r &
<*i*> ^ q <> <*i*> ^ r )
by A3, FINSEQ_1:33, TREES_1:1;
then
(
x is_a_proper_prefix_of <*i*> ^ r &
<*i*> ^ r in tree p )
by A2, A3, XBOOLE_0:def 8, TREES_3:def 15;
hence
contradiction
by A1, TREES_1:def 5;
verum end; hence
a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
by A2, AB;
verum end;
end;
let x be object ; TARSKI:def 3 ( not x in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } or x in Leaves (tree p) )
assume
x in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
; x in Leaves (tree p)
then consider i being Nat, q being FinSequence of NAT , d being Tree such that
B1:
( x = <*i*> ^ q & q in Leaves d & i + 1 in dom p & d = p . (i + 1) )
;
i + 1 <= len p
by B1, FINSEQ_3:25;
then
i < len p
by NAT_1:13;
then reconsider r = x as Element of tree p by B1, TREES_3:48;
assume
x nin Leaves (tree p)
; contradiction
then consider q0 being FinSequence of NAT such that
B4:
( q0 in tree p & r is_a_proper_prefix_of q0 )
by TREES_1:def 5;
consider w being FinSequence such that
B6:
q0 = (<*i*> ^ q) ^ w
by B1, B4, XBOOLE_0:def 8, TREES_1:1;
B7:
q0 = <*i*> ^ (q ^ w)
by B6, FINSEQ_1:32;
then B9:
q ^ w is FinSequence of NAT
by FINSEQ_1:36;
( q ^ w in d & q is_a_proper_prefix_of q ^ w )
by B1, B4, B7, TREES_3:48, TREES_1:49;
hence
contradiction
by B1, B9, TREES_1:def 5; verum