let T, T1 be Tree; :: thesis: for P being AntiChain_of_Prefixes of T

for p being FinSequence of NAT st p in P holds

T1 = (tree (T,P,T1)) | p

let P be AntiChain_of_Prefixes of T; :: thesis: for p being FinSequence of NAT st p in P holds

T1 = (tree (T,P,T1)) | p

let p be FinSequence of NAT ; :: thesis: ( p in P implies T1 = (tree (T,P,T1)) | p )

assume A1: p in P ; :: thesis: T1 = (tree (T,P,T1)) | p

ex q, r being FinSequence of NAT st

( q in P & r in T1 & p = q ^ r )

let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in T1 or x in (tree (T,P,T1)) | p ) & ( not x in (tree (T,P,T1)) | p or x in T1 ) )

thus ( x in T1 implies x in (tree (T,P,T1)) | p ) :: thesis: ( not x in (tree (T,P,T1)) | p or x in T1 )

for p being FinSequence of NAT st p in P holds

T1 = (tree (T,P,T1)) | p

let P be AntiChain_of_Prefixes of T; :: thesis: for p being FinSequence of NAT st p in P holds

T1 = (tree (T,P,T1)) | p

let p be FinSequence of NAT ; :: thesis: ( p in P implies T1 = (tree (T,P,T1)) | p )

assume A1: p in P ; :: thesis: T1 = (tree (T,P,T1)) | p

ex q, r being FinSequence of NAT st

( q in P & r in T1 & p = q ^ r )

proof

then A5:
p in tree (T,P,T1)
by Def1;
consider q being FinSequence of NAT such that

A2: q = p ;

consider r being FinSequence of NAT such that

A3: r = <*> NAT ;

A4: r in T1 by A3, TREES_1:22;

p = q ^ r by A2, A3, FINSEQ_1:34;

hence ex q, r being FinSequence of NAT st

( q in P & r in T1 & p = q ^ r ) by A1, A2, A4; :: thesis: verum

end;A2: q = p ;

consider r being FinSequence of NAT such that

A3: r = <*> NAT ;

A4: r in T1 by A3, TREES_1:22;

p = q ^ r by A2, A3, FINSEQ_1:34;

hence ex q, r being FinSequence of NAT st

( q in P & r in T1 & p = q ^ r ) by A1, A2, A4; :: thesis: verum

let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in T1 or x in (tree (T,P,T1)) | p ) & ( not x in (tree (T,P,T1)) | p or x in T1 ) )

thus ( x in T1 implies x in (tree (T,P,T1)) | p ) :: thesis: ( not x in (tree (T,P,T1)) | p or x in T1 )

proof

thus
( x in (tree (T,P,T1)) | p implies x in T1 )
:: thesis: verum
assume
x in T1
; :: thesis: x in (tree (T,P,T1)) | p

then p ^ x in tree (T,P,T1) by A1, Def1;

hence x in (tree (T,P,T1)) | p by A5, TREES_1:def 6; :: thesis: verum

end;then p ^ x in tree (T,P,T1) by A1, Def1;

hence x in (tree (T,P,T1)) | p by A5, TREES_1:def 6; :: thesis: verum

proof

assume
x in (tree (T,P,T1)) | p
; :: thesis: x in T1

then A6: p ^ x in tree (T,P,T1) by A5, TREES_1:def 6;

end;then A6: p ^ x in tree (T,P,T1) by A5, TREES_1:def 6;

A7: now :: thesis: ( p ^ x in T & ( for r being FinSequence of NAT st r in P holds

not r is_a_proper_prefix_of p ^ x ) implies x in T1 )

not r is_a_proper_prefix_of p ^ x ) implies x in T1 )

assume that

p ^ x in T and

A8: for r being FinSequence of NAT st r in P holds

not r is_a_proper_prefix_of p ^ x ; :: thesis: x in T1

A9: not p is_a_proper_prefix_of p ^ x by A1, A8;

p is_a_prefix_of p ^ x by TREES_1:1;

then p ^ x = p by A9

.= p ^ (<*> NAT) by FINSEQ_1:34 ;

then x = {} by FINSEQ_1:33;

hence x in T1 by TREES_1:22; :: thesis: verum

end;p ^ x in T and

A8: for r being FinSequence of NAT st r in P holds

not r is_a_proper_prefix_of p ^ x ; :: thesis: x in T1

A9: not p is_a_proper_prefix_of p ^ x by A1, A8;

p is_a_prefix_of p ^ x by TREES_1:1;

then p ^ x = p by A9

.= p ^ (<*> NAT) by FINSEQ_1:34 ;

then x = {} by FINSEQ_1:33;

hence x in T1 by TREES_1:22; :: thesis: verum

now :: thesis: ( ex s, r being FinSequence of NAT st

( s in P & r in T1 & p ^ x = s ^ r ) implies x in T1 )

hence
x in T1
by A1, A6, A7, Def1; :: thesis: verum( s in P & r in T1 & p ^ x = s ^ r ) implies x in T1 )

given s, r being FinSequence of NAT such that A10:
s in P
and

A11: r in T1 and

A12: p ^ x = s ^ r ; :: thesis: x in T1

end;A11: r in T1 and

A12: p ^ x = s ^ r ; :: thesis: x in T1

now :: thesis: not s <> p

hence
x in T1
by A11, A12, FINSEQ_1:33; :: thesis: verumassume
s <> p
; :: thesis: contradiction

then not s,p are_c=-comparable by A1, A10, TREES_1:def 10;

hence contradiction by A12, Th1; :: thesis: verum

end;then not s,p are_c=-comparable by A1, A10, TREES_1:def 10;

hence contradiction by A12, Th1; :: thesis: verum