let Z1, Z2 be Tree; :: thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
let p be FinSequence of NAT ; :: thesis: ( p in Z1 implies for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w )
assume A1: p in Z1 ; :: thesis: for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
set Z = Z1 with-replacement p,Z2;
let v be Element of Z1 with-replacement p,Z2; :: thesis: for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds
succ v = succ w
let w be Element of Z1; :: thesis: ( v = w & w is_a_proper_prefix_of p implies succ v = succ w )
assume A2: ( v = w & w is_a_proper_prefix_of p ) ; :: thesis: succ v = succ w
then ( w is_a_prefix_of p & w <> p ) by XBOOLE_0:def 8;
then consider r being FinSequence such that
A3: p = w ^ r by TREES_1:8;

now

let n be Nat; :: thesis: ( n in dom r implies r . n in NAT )
assume A4: n in dom r ; :: thesis: r . n in NAT
then A5: p . ((len w) + n) = r . n by A3, FINSEQ_1:def 7;
(len w) + n in dom p by A3, A4, FINSEQ_1:41;
then p . ((len w) + n) in rng p by FUNCT_1:def 5;
hence r . n in NAT by A5; :: thesis: verum

end;

then reconsider r = r as FinSequence of NAT by FINSEQ_2:14;
A6: r <> {} by A2, A3, FINSEQ_1:47;

now

let x be set ; :: thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) )
thus ( x in succ v implies x in succ w ) :: thesis: ( x in succ w implies x in succ v )

proof

assume x in succ v ; :: thesis: x in succ w
then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement p,Z2 } by TREES_2:def 5;
then consider n being Element of NAT such that
A7: ( x = v ^ <*n*> & v ^ <*n*> in Z1 with-replacement p,Z2 ) ;
reconsider x' = x as FinSequence of NAT by A7;

now

per cases ( ( x' in Z1 & not p is_a_proper_prefix_of x' ) or ex r being FinSequence of NAT st
( r in Z2 & x' = p ^ r ) ) by A1, A7, TREES_1:def 12;

suppose ( x' in Z1 & not p is_a_proper_prefix_of x' ) ; :: thesis: x in succ w

then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A7;
hence x in succ w by TREES_2:def 5; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in Z2 & x' = p ^ r ) ; :: thesis: x in succ w

then consider s being FinSequence of NAT such that
A8: ( s in Z2 & v ^ <*n*> = p ^ s ) by A7;
w ^ <*n*> = w ^ (r ^ s) by A2, A3, A8, FINSEQ_1:45;
then A9: <*n*> = r ^ s by FINSEQ_1:46;
s = {}

proof

assume not s = {} ; :: thesis: contradiction
then len s <> 0 ;
then len s > 0 by NAT_1:3;
then A10: 0 + 1 <= len s by NAT_1:13;
len r <> 0 by A6;
then len r > 0 by NAT_1:3;
then 0 + 1 <= len r by NAT_1:13;
then 1 + 1 <= (len r) + (len s) by A10, XREAL_1:9;
then 2 <= len <*n*> by A9, FINSEQ_1:35;
then 2 <= 1 by FINSEQ_1:56;
hence contradiction ; :: thesis: verum

end;

then <*n*> = r by A9, FINSEQ_1:47;
then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A1, A2, A3, A7;
hence x in succ w by TREES_2:def 5; :: thesis: verum

end;

end;

end;

hence x in succ w ; :: thesis: verum

end;

assume x in succ w ; :: thesis: x in succ v
then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def 5;
then consider n being Element of NAT such that
A11: ( x = w ^ <*n*> & w ^ <*n*> in Z1 ) ;

now

assume A12: not v ^ <*n*> in Z1 with-replacement p,Z2 ; :: thesis: contradiction

now

per cases ( not v ^ <*n*> in Z1 or p is_a_proper_prefix_of v ^ <*n*> ) by A1, A12, TREES_1:def 12;

suppose not v ^ <*n*> in Z1 ; :: thesis: contradiction

hence contradiction by A2, A11; :: thesis: verum

end;

suppose p is_a_proper_prefix_of v ^ <*n*> ; :: thesis: contradiction

then r is_a_proper_prefix_of <*n*> by A2, A3, TREES_1:86;
then r in ProperPrefixes <*n*> by TREES_1:36;
then r in {{} } by TREES_1:40;
hence contradiction by A6, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement p,Z2 } by A2, A11;
hence x in succ v by TREES_2:def 5; :: thesis: verum

end;

hence succ v = succ w by TARSKI:2; :: thesis: verum