let p, q be Tree-yielding FinSequence; :: thesis: for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Nat st i in dom p & i <> k + 1 holds

p . i = q . i ) holds

for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

let k be Element of NAT ; :: thesis: ( len p = len q & k + 1 in dom p & ( for i being Nat st i in dom p & i <> k + 1 holds

p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t) )

assume that

A1: len p = len q and

A2: k + 1 in dom p and

A3: for i being Nat st i in dom p & i <> k + 1 holds

p . i = q . i ; :: thesis: for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

let t be Tree; :: thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement (<*k*>,t) )

set o = <*k*>;

k + 1 <= len p by A2, FINSEQ_3:25;

then A4: k < len p by NAT_1:13;

assume A5: q . (k + 1) = t ; :: thesis: tree q = (tree p) with-replacement (<*k*>,t)

then A21: {} in p . (k + 1) by TREES_1:22;

<*k*> = <*k*> ^ {} by FINSEQ_1:34;

then <*k*> in tree p by A4, A21, TREES_3:def 15;

hence tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def 9; :: thesis: verum

p . i = q . i ) holds

for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

let k be Element of NAT ; :: thesis: ( len p = len q & k + 1 in dom p & ( for i being Nat st i in dom p & i <> k + 1 holds

p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t) )

assume that

A1: len p = len q and

A2: k + 1 in dom p and

A3: for i being Nat st i in dom p & i <> k + 1 holds

p . i = q . i ; :: thesis: for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

let t be Tree; :: thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement (<*k*>,t) )

set o = <*k*>;

k + 1 <= len p by A2, FINSEQ_3:25;

then A4: k < len p by NAT_1:13;

assume A5: q . (k + 1) = t ; :: thesis: tree q = (tree p) with-replacement (<*k*>,t)

A6: now :: thesis: for s being FinSequence of NAT holds

( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) implies s in tree q ) )

p . (k + 1) is Tree
by A2, TREES_3:22;( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) implies s in tree q ) )

let s be FinSequence of NAT ; :: thesis: ( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) implies b_{1} in tree q ) )

( r in t & s = <*k*> ^ r ) ) ; :: thesis: b_{1} in tree q

end;( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) implies b

hereby :: thesis: ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) implies b_{1} in tree q )

assume A13:
( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) implies b

assume A7:
s in tree q
; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) )

end;( r in t & s = <*k*> ^ r ) )

per cases
( s = {} or ex n being Nat ex r being FinSequence st

( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ) by A7, TREES_3:def 15;

end;

( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ) by A7, TREES_3:def 15;

suppose
s = {}
; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) )

( r in t & s = <*k*> ^ r ) )

hence
( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) by TREES_1:22; :: thesis: verum

end;( r in t & s = <*k*> ^ r ) ) by TREES_1:22; :: thesis: verum

suppose
ex n being Nat ex r being FinSequence st

( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) )

( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) )

then consider n being Nat, r being FinSequence such that

A8: n < len q and

A9: r in q . (n + 1) and

A10: s = <*n*> ^ r ;

( r in t & s = <*k*> ^ r ) ) ; :: thesis: verum

end;A8: n < len q and

A9: r in q . (n + 1) and

A10: s = <*n*> ^ r ;

now :: thesis: ( ( n = k & ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) or ( n <> k & s in tree p & not <*k*> is_a_proper_prefix_of s ) )end;

hence
( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) or ( n <> k & s in tree p & not <*k*> is_a_proper_prefix_of s ) )

per cases
( n = k or n <> k )
;

end;

case A11:
n = k
; :: thesis: ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r )

( r in t & s = <*k*> ^ r )

reconsider r = r as FinSequence of NAT by A10, FINSEQ_1:36;

take r = r; :: thesis: ( r in t & s = <*k*> ^ r )

thus ( r in t & s = <*k*> ^ r ) by A5, A9, A10, A11; :: thesis: verum

end;take r = r; :: thesis: ( r in t & s = <*k*> ^ r )

thus ( r in t & s = <*k*> ^ r ) by A5, A9, A10, A11; :: thesis: verum

case A12:
n <> k
; :: thesis: ( s in tree p & not <*k*> is_a_proper_prefix_of s )

( 1 <= n + 1 & n + 1 <= len p )
by A1, A8, NAT_1:11, NAT_1:13;

then n + 1 in dom p by FINSEQ_3:25;

then q . (n + 1) = p . (n + 1) by A3, A12, XCMPLX_1:2;

hence s in tree p by A1, A8, A9, A10, TREES_3:def 15; :: thesis: not <*k*> is_a_proper_prefix_of s

assume <*k*> is_a_proper_prefix_of s ; :: thesis: contradiction

then <*k*> is_a_prefix_of s ;

then ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:1;

then k = s . 1 by FINSEQ_1:41

.= n by A10, FINSEQ_1:41 ;

hence contradiction by A12; :: thesis: verum

end;then n + 1 in dom p by FINSEQ_3:25;

then q . (n + 1) = p . (n + 1) by A3, A12, XCMPLX_1:2;

hence s in tree p by A1, A8, A9, A10, TREES_3:def 15; :: thesis: not <*k*> is_a_proper_prefix_of s

assume <*k*> is_a_proper_prefix_of s ; :: thesis: contradiction

then <*k*> is_a_prefix_of s ;

then ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:1;

then k = s . 1 by FINSEQ_1:41

.= n by A10, FINSEQ_1:41 ;

hence contradiction by A12; :: thesis: verum

( r in t & s = <*k*> ^ r ) ) ; :: thesis: verum

( r in t & s = <*k*> ^ r ) ) ; :: thesis: b

per cases
( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ) by A13;

end;

( r in t & s = <*k*> ^ r ) ) by A13;

suppose that A14:
s in tree p
and

A15: not <*k*> is_a_proper_prefix_of s ; :: thesis: b_{1} in tree q

end;

A15: not <*k*> is_a_proper_prefix_of s ; :: thesis: b

now :: thesis: s in tree qend;

hence
s in tree q
; :: thesis: verumper cases
( s = {} or ex n being Nat ex r being FinSequence st

( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ) by A14, TREES_3:def 15;

end;

( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ) by A14, TREES_3:def 15;

suppose
ex n being Nat ex r being FinSequence st

( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ; :: thesis: s in tree q

( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ; :: thesis: s in tree q

then consider n being Nat, r being FinSequence such that

A16: n < len p and

A17: r in p . (n + 1) and

A18: s = <*n*> ^ r ;

end;A16: n < len p and

A17: r in p . (n + 1) and

A18: s = <*n*> ^ r ;

now :: thesis: s in tree qend;

hence
s in tree q
; :: thesis: verumper cases
( r = {} or r <> {} )
;

end;

suppose A19:
r = {}
; :: thesis: s in tree q

( 1 <= n + 1 & n + 1 <= len q )
by A1, A16, NAT_1:11, NAT_1:13;

then n + 1 in dom q by FINSEQ_3:25;

then q . (n + 1) is Tree by TREES_3:22;

then r in q . (n + 1) by A19, TREES_1:22;

hence s in tree q by A1, A16, A18, TREES_3:def 15; :: thesis: verum

end;then n + 1 in dom q by FINSEQ_3:25;

then q . (n + 1) is Tree by TREES_3:22;

then r in q . (n + 1) by A19, TREES_1:22;

hence s in tree q by A1, A16, A18, TREES_3:def 15; :: thesis: verum

suppose
r <> {}
; :: thesis: s in tree q

then A20:
n <> k
by A15, A18, FINSEQ_1:87, TREES_1:1;

( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13;

then n + 1 in dom p by FINSEQ_3:25;

then q . (n + 1) = p . (n + 1) by A3, A20, XCMPLX_1:2;

hence s in tree q by A1, A16, A17, A18, TREES_3:def 15; :: thesis: verum

end;( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13;

then n + 1 in dom p by FINSEQ_3:25;

then q . (n + 1) = p . (n + 1) by A3, A20, XCMPLX_1:2;

hence s in tree q by A1, A16, A17, A18, TREES_3:def 15; :: thesis: verum

suppose
ex r being FinSequence of NAT st

( r in t & s = <*k*> ^ r ) ; :: thesis: b_{1} in tree q

end;

( r in t & s = <*k*> ^ r ) ; :: thesis: b

end;

then A21: {} in p . (k + 1) by TREES_1:22;

<*k*> = <*k*> ^ {} by FINSEQ_1:34;

then <*k*> in tree p by A4, A21, TREES_3:def 15;

hence tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def 9; :: thesis: verum