let t, t1 be Tree; :: thesis: for p, q being FinSequence of NAT st p in t & q in t with-replacement (p,t1) holds
( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds
r in t1 ) )
let p, q be FinSequence of NAT ; :: thesis: ( p in t & q in t with-replacement (p,t1) implies ( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds
r in t1 ) ) )
assume Z0: p in t ; :: thesis: ( not q in t with-replacement (p,t1) or ( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds
r in t1 ) ) )
assume Z1: q in t with-replacement (p,t1) ; :: thesis: ( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds
r in t1 ) )
thus ( not p is_a_prefix_of q implies q in t ) :: thesis: for r being FinSequence of NAT st q = p ^ r holds
r in t1
proof
assume not p is_a_prefix_of q ; :: thesis: q in t
then for r being FinSequence of NAT holds
( not r in t1 or not q = p ^ r ) by TREES_1:1;
hence q in t by Z0, Z1, TREES_1:def 9; :: thesis: verum
end;
let r be FinSequence of NAT ; :: thesis: ( q = p ^ r implies r in t1 )
assume Z3: q = p ^ r ; :: thesis: r in t1
then p c= q by TREES_1:1;
then ( p c< q or ( p = q & p = p ^ {} ) ) by XBOOLE_0:def 8, FINSEQ_1:34;
then ex r being FinSequence of NAT st
( r in t1 & q = p ^ r ) by Z0, Z1, TREES_1:22, TREES_1:def 9;
hence r in t1 by Z3, FINSEQ_1:33; :: thesis: verum