let p be FinSequence of NAT ; :: thesis: for T, T1 being Tree st p in T holds
T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum }
let T, T1 be Tree; :: thesis: ( p in T implies T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum } )
assume A1: p in T ; :: thesis: T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum }
thus T with-replacement (p,T1) c= { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum } :: according to XBOOLE_0:def 10 :: thesis: { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum } is_a_prefix_of T with-replacement (p,T1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T with-replacement (p,T1) or x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum } )
assume A2: x in T with-replacement (p,T1) ; :: thesis: x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum }
then reconsider q = x as FinSequence of NAT by Th18;
A3: ( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies x in { (p ^ s) where s is Element of T1 : verum } ) ;
( q in T & not p is_a_proper_prefix_of q implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) ;
hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum } by A1, A2, A3, Def9, XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum } or x in T with-replacement (p,T1) )
assume A4: x in { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum } ; :: thesis: x in T with-replacement (p,T1)
A5: now :: thesis: ( x in { (p ^ s) where s is Element of T1 : verum } implies x in T with-replacement (p,T1) )
assume x in { (p ^ s) where s is Element of T1 : verum } ; :: thesis: x in T with-replacement (p,T1)
then ex s being Element of T1 st x = p ^ s ;
hence x in T with-replacement (p,T1) by A1, Def9; :: thesis: verum
end;
now :: thesis: ( x in { t where t is Element of T : not p is_a_proper_prefix_of t } implies x in T with-replacement (p,T1) )
assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: x in T with-replacement (p,T1)
then ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence x in T with-replacement (p,T1) by A1, Def9; :: thesis: verum
end;
hence x in T with-replacement (p,T1) by A4, A5, XBOOLE_0:def 3; :: thesis: verum