let T, T1 be Tree; :: thesis: for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)
let t be Element of T; :: thesis: tree (T,{t},T1) = T with-replacement (t,T1)
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in tree (T,{t},T1) or p in T with-replacement (t,T1) ) & ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) ) )
thus ( p in tree (T,{t},T1) implies p in T with-replacement (t,T1) ) :: thesis: ( not p in T with-replacement (t,T1) or p in tree (T,{t},T1) )
proof
assume A1: p in tree (T,{t},T1) ; :: thesis: p in T with-replacement (t,T1)
A2: now :: thesis: ( p in T & ( for s being FinSequence of NAT st s in {t} holds
not s is_a_proper_prefix_of p ) implies ( p in T & not t is_a_proper_prefix_of p ) )
assume A3: ( p in T & ( for s being FinSequence of NAT st s in {t} holds
not s is_a_proper_prefix_of p ) ) ; :: thesis: ( p in T & not t is_a_proper_prefix_of p )
t in {t} by TARSKI:def 1;
hence ( p in T & not t is_a_proper_prefix_of p ) by A3; :: thesis: verum
end;
now :: thesis: ( ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) implies ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) )
given s being FinSequence of NAT such that A4: ex r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) ; :: thesis: ex r being FinSequence of NAT st
( r in T1 & p = t ^ r )
s = t by A4, TARSKI:def 1;
hence ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) by A4; :: thesis: verum
end;
hence p in T with-replacement (t,T1) by A1, A2, Def1, TREES_1:def 9; :: thesis: verum
end;
assume A5: p in T with-replacement (t,T1) ; :: thesis: p in tree (T,{t},T1)
A6: ( p in T & not t is_a_proper_prefix_of p implies ( p in T & ( for s being FinSequence of NAT st s in {t} holds
not s is_a_proper_prefix_of p ) ) ) by TARSKI:def 1;
now :: thesis: ( ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) implies ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) )
assume A7: ex r being FinSequence of NAT st
( r in T1 & p = t ^ r ) ; :: thesis: ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r )
thus ex s, r being FinSequence of NAT st
( s in {t} & r in T1 & p = s ^ r ) :: thesis: verum
proof
take t ; :: thesis: ex r being FinSequence of NAT st
( t in {t} & r in T1 & p = t ^ r )
t in {t} by TARSKI:def 1;
hence ex r being FinSequence of NAT st
( t in {t} & r in T1 & p = t ^ r ) by A7; :: thesis: verum
end;
end;
hence p in tree (T,{t},T1) by A5, A6, Def1, TREES_1:def 9; :: thesis: verum