MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wrd2ind Structured version   Unicode version

Theorem wrd2ind 12364
Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.)
Hypotheses
Ref Expression
wrd2ind.1  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ( ph 
<->  ps ) )
wrd2ind.2  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ph  <->  ch )
)
wrd2ind.3  |-  ( ( x  =  ( y concat  <" z "> )  /\  w  =  ( u concat  <" s "> ) )  -> 
( ph  <->  th ) )
wrd2ind.4  |-  ( x  =  A  ->  ( rh 
<->  ta ) )
wrd2ind.5  |-  ( w  =  B  ->  ( ph 
<->  rh ) )
wrd2ind.6  |-  ps
wrd2ind.7  |-  ( ( ( y  e. Word  X  /\  z  e.  X
)  /\  ( u  e. Word  Y  /\  s  e.  Y )  /\  ( # `
 y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
Assertion
Ref Expression
wrd2ind  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ta )
Distinct variable groups:    x, w, A    y, w, z, B, x    u, s, w, x, y, z, X    Y, s, u, w, x, y, z    ch, w, x    ph, s, u, y, z    ta, x    th, w, x    rh, w
Allowed substitution hints:    ph( x, w)    ps( x, y, z, w, u, s)    ch( y,
z, u, s)    th( y,
z, u, s)    ta( y, z, w, u, s)    rh( x, y, z, u, s)    A( y, z, u, s)    B( u, s)

Proof of Theorem wrd2ind
Dummy variables  n  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lencl 12241 . . . . 5  |-  ( A  e. Word  X  ->  ( # `
 A )  e. 
NN0 )
2 eqeq2 2446 . . . . . . . . 9  |-  ( n  =  0  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  0 ) )
32anbi2d 703 . . . . . . . 8  |-  ( n  =  0  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 ) ) )
43imbi1d 317 . . . . . . 7  |-  ( n  =  0  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 )  ->  ph ) ) )
542ralbidv 2751 . . . . . 6  |-  ( n  =  0  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  0 )  ->  ph )
) )
6 eqeq2 2446 . . . . . . . . 9  |-  ( n  =  m  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  m ) )
76anbi2d 703 . . . . . . . 8  |-  ( n  =  m  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  m ) ) )
87imbi1d 317 . . . . . . 7  |-  ( n  =  m  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph ) ) )
982ralbidv 2751 . . . . . 6  |-  ( n  =  m  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  m )  ->  ph )
) )
10 eqeq2 2446 . . . . . . . . 9  |-  ( n  =  ( m  + 
1 )  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  ( m  +  1 ) ) )
1110anbi2d 703 . . . . . . . 8  |-  ( n  =  ( m  + 
1 )  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )
1211imbi1d 317 . . . . . . 7  |-  ( n  =  ( m  + 
1 )  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) ) )
13122ralbidv 2751 . . . . . 6  |-  ( n  =  ( m  + 
1 )  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ph )
) )
14 eqeq2 2446 . . . . . . . . 9  |-  ( n  =  ( # `  A
)  ->  ( ( # `
 x )  =  n  <->  ( # `  x
)  =  ( # `  A ) ) )
1514anbi2d 703 . . . . . . . 8  |-  ( n  =  ( # `  A
)  ->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  n )  <-> 
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) ) ) )
1615imbi1d 317 . . . . . . 7  |-  ( n  =  ( # `  A
)  ->  ( (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )
) )
17162ralbidv 2751 . . . . . 6  |-  ( n  =  ( # `  A
)  ->  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) ) )
18 eqeq1 2443 . . . . . . . . . . . 12  |-  ( (
# `  x )  =  0  ->  (
( # `  x )  =  ( # `  w
)  <->  0  =  (
# `  w )
) )
1918adantl 466 . . . . . . . . . . 11  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( ( # `  x )  =  (
# `  w )  <->  0  =  ( # `  w
) ) )
20 eqcom 2439 . . . . . . . . . . . . . . 15  |-  ( 0  =  ( # `  w
)  <->  ( # `  w
)  =  0 )
21 hasheq0 12123 . . . . . . . . . . . . . . 15  |-  ( w  e. Word  Y  ->  (
( # `  w )  =  0  <->  w  =  (/) ) )
2220, 21syl5bb 257 . . . . . . . . . . . . . 14  |-  ( w  e. Word  Y  ->  (
0  =  ( # `  w )  <->  w  =  (/) ) )
23 hasheq0 12123 . . . . . . . . . . . . . . . 16  |-  ( x  e. Word  X  ->  (
( # `  x )  =  0  <->  x  =  (/) ) )
24 wrd2ind.6 . . . . . . . . . . . . . . . . . 18  |-  ps
25 wrd2ind.1 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ( ph 
<->  ps ) )
2624, 25mpbiri 233 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ph )
2726ex 434 . . . . . . . . . . . . . . . 16  |-  ( x  =  (/)  ->  ( w  =  (/)  ->  ph )
)
2823, 27syl6bi 228 . . . . . . . . . . . . . . 15  |-  ( x  e. Word  X  ->  (
( # `  x )  =  0  ->  (
w  =  (/)  ->  ph )
) )
2928com13 80 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( (
# `  x )  =  0  ->  (
x  e. Word  X  ->  ph ) ) )
3022, 29syl6bi 228 . . . . . . . . . . . . 13  |-  ( w  e. Word  Y  ->  (
0  =  ( # `  w )  ->  (
( # `  x )  =  0  ->  (
x  e. Word  X  ->  ph ) ) ) )
3130com24 87 . . . . . . . . . . . 12  |-  ( w  e. Word  Y  ->  (
x  e. Word  X  ->  ( ( # `  x
)  =  0  -> 
( 0  =  (
# `  w )  ->  ph ) ) ) )
3231imp31 432 . . . . . . . . . . 11  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( 0  =  ( # `  w
)  ->  ph ) )
3319, 32sylbid 215 . . . . . . . . . 10  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( ( # `  x )  =  (
# `  w )  ->  ph ) )
3433ex 434 . . . . . . . . 9  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( # `  x
)  =  0  -> 
( ( # `  x
)  =  ( # `  w )  ->  ph )
) )
3534com23 78 . . . . . . . 8  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( # `  x
)  =  ( # `  w )  ->  (
( # `  x )  =  0  ->  ph )
) )
3635impd 431 . . . . . . 7  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  0 )  ->  ph ) )
3736rgen2 2806 . . . . . 6  |-  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 )  ->  ph )
38 fveq2 5684 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( # `
 x )  =  ( # `  y
) )
39 fveq2 5684 . . . . . . . . . . . . 13  |-  ( w  =  u  ->  ( # `
 w )  =  ( # `  u
) )
4038, 39eqeqan12d 2452 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( # `  x
)  =  ( # `  w )  <->  ( # `  y
)  =  ( # `  u ) ) )
4138eqeq1d 2445 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( # `  x )  =  m  <->  ( # `  y
)  =  m ) )
4241adantr 465 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( # `  x
)  =  m  <->  ( # `  y
)  =  m ) )
4340, 42anbi12d 710 . . . . . . . . . . 11  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  m )  <-> 
( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m ) ) )
44 wrd2ind.2 . . . . . . . . . . 11  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ph  <->  ch )
)
4543, 44imbi12d 320 . . . . . . . . . 10  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  ( (
( # `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) ) )
4645ancoms 453 . . . . . . . . 9  |-  ( ( w  =  u  /\  x  =  y )  ->  ( ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  ( (
( # `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) ) )
4746cbvraldva 2947 . . . . . . . 8  |-  ( w  =  u  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  m )  ->  ph )  <->  A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) ) )
4847cbvralv 2941 . . . . . . 7  |-  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) )
49 swrdcl 12307 . . . . . . . . . . . . . . . . 17  |-  ( w  e. Word  Y  ->  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y )
5049adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y
)
5150ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y )
52 wrdf 12232 . . . . . . . . . . . . . . . . . 18  |-  ( w  e. Word  Y  ->  w : ( 0..^ (
# `  w )
) --> Y )
5352adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  w : ( 0..^ ( # `  w
) ) --> Y )
5453ad2antrl 727 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w : ( 0..^ (
# `  w )
) --> Y )
55 eqeq1 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  =  ( # `  w
)  <->  ( m  + 
1 )  =  (
# `  w )
) )
56 nn0p1nn 10611 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  NN )
57 eleq1 2497 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  w )  =  ( m  + 
1 )  ->  (
( # `  w )  e.  NN  <->  ( m  +  1 )  e.  NN ) )
5857eqcoms 2440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  =  ( # `  w
)  ->  ( ( # `
 w )  e.  NN  <->  ( m  + 
1 )  e.  NN ) )
5956, 58syl5ibr 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  +  1 )  =  ( # `  w
)  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) )
6055, 59syl6bi 228 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  =  ( # `  w
)  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) ) )
6160impcom 430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  (
m  e.  NN0  ->  (
# `  w )  e.  NN ) )
6261adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) )  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) )
6362impcom 430 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  e.  NN )
64 fzo0end 11611 . . . . . . . . . . . . . . . . 17  |-  ( (
# `  w )  e.  NN  ->  ( ( # `
 w )  - 
1 )  e.  ( 0..^ ( # `  w
) ) )
6563, 64syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  w )  -  1 )  e.  ( 0..^ ( # `  w ) ) )
6654, 65ffvelrnd 5837 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w `  ( ( # `
 w )  - 
1 ) )  e.  Y )
6751, 66jca 532 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y  /\  ( w `  (
( # `  w )  -  1 ) )  e.  Y ) )
68 swrdcl 12307 . . . . . . . . . . . . . . . 16  |-  ( x  e. Word  X  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
6968adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X
)
7069ad2antrl 727 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
71 wrdf 12232 . . . . . . . . . . . . . . . . 17  |-  ( x  e. Word  X  ->  x : ( 0..^ (
# `  x )
) --> X )
7271adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  x : ( 0..^ ( # `  x
) ) --> X )
7372ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x : ( 0..^ (
# `  x )
) --> X )
74 eleq1 2497 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  e.  NN  <->  ( m  +  1 )  e.  NN ) )
7556, 74syl5ibr 221 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
m  e.  NN0  ->  (
# `  x )  e.  NN ) )
7675ad2antll 728 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) )  ->  ( m  e.  NN0  ->  ( # `  x
)  e.  NN ) )
7776impcom 430 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  e.  NN )
78 fzo0end 11611 . . . . . . . . . . . . . . . 16  |-  ( (
# `  x )  e.  NN  ->  ( ( # `
 x )  - 
1 )  e.  ( 0..^ ( # `  x
) ) )
7977, 78syl 16 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  e.  ( 0..^ ( # `  x ) ) )
8073, 79ffvelrnd 5837 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
x `  ( ( # `
 x )  - 
1 ) )  e.  X )
8167, 70, 80jca32 535 . . . . . . . . . . . . 13  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( w `  (
( # `  w )  -  1 ) )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( x `  (
( # `  x )  -  1 ) )  e.  X ) ) )
8281adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( w `  (
( # `  w )  -  1 ) )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( x `  (
( # `  x )  -  1 ) )  e.  X ) ) )
83 simprl 755 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w  e. Word  Y  /\  x  e. Word  X )
)
84 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) )
85 simprrl 763 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  =  ( # `  w
) )
8685oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  =  ( ( # `  w
)  -  1 ) )
87 simprlr 762 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  e. Word  X )
88 fzossfz 11562 . . . . . . . . . . . . . . . . . 18  |-  ( 0..^ ( # `  x
) )  C_  (
0 ... ( # `  x
) )
89 simprrr 764 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  =  ( m  +  1 ) )
9056ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
m  +  1 )  e.  NN )
9189, 90eqeltrd 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  e.  NN )
9291, 78syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  e.  ( 0..^ ( # `  x ) ) )
9388, 92sseldi 3347 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  e.  ( 0 ... ( # `
 x ) ) )
94 swrd0len 12310 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e. Word  X  /\  ( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) )  -> 
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  ( ( # `  x
)  -  1 ) )
9587, 93, 94syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( ( # `  x
)  -  1 ) )
96 simprll 761 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  e. Word  Y )
97 oveq1 6093 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( ( # `
 w )  - 
1 )  =  ( ( # `  x
)  -  1 ) )
98 oveq2 6094 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( 0 ... ( # `  w
) )  =  ( 0 ... ( # `  x ) ) )
9997, 98eleq12d 2505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) )  <-> 
( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) ) )
10099eqcoms 2440 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  x )  =  ( # `  w
)  ->  ( (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) )  <-> 
( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) ) )
101100adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  (
( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) )  <->  ( ( # `
 x )  - 
1 )  e.  ( 0 ... ( # `  x ) ) ) )
102101ad2antll 728 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) )  <->  ( ( # `
 x )  - 
1 )  e.  ( 0 ... ( # `  x ) ) ) )
10393, 102mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) ) )
104 swrd0len 12310 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e. Word  Y  /\  ( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) ) )  -> 
( # `  ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) )  =  ( ( # `  w
)  -  1 ) )
10596, 103, 104syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) )  =  ( ( # `  w
)  -  1 ) )
10686, 95, 1053eqtr4d 2479 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )
10789oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  =  ( ( m  + 
1 )  -  1 ) )
108 nn0cn 10581 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN0  ->  m  e.  CC )
109108ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  m  e.  CC )
110 ax-1cn 9332 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
111 pncan 9608 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
112109, 110, 111sylancl 662 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( m  +  1 )  -  1 )  =  m )
11395, 107, 1123eqtrd 2473 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )
114106, 113jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m ) )
11569adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
116 fveq2 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( # `
 y )  =  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ) )
117 fveq2 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( # `
 u )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )
118116, 117eqeqan12d 2452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
( # `  y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
119118expcom 435 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  ->  ( ( # `
 y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
120119adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  ->  ( ( # `
 y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
121120imp 429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( # `  y
)  =  ( # `  u )  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
122116eqeq1d 2445 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( # `  y )  =  m  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  m ) )
123122adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( # `  y
)  =  m  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  m ) )
124121, 123anbi12d 710 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( ( # `  y )  =  (
# `  u )  /\  ( # `  y
)  =  m )  <-> 
( ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m ) ) )
125 vex 2969 . . . . . . . . . . . . . . . . . . . . 21  |-  y  e. 
_V
126 vex 2969 . . . . . . . . . . . . . . . . . . . . 21  |-  u  e. 
_V
127125, 126, 44sbc2ie 3255 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. y  /  x ]. [. u  /  w ]. ph  <->  ch )
128127bicomi 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ch  <->  [. y  /  x ]. [. u  /  w ]. ph )
129128a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ch  <->  [. y  /  x ]. [. u  /  w ]. ph ) )
130 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )
131130sbceq1d 3184 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( [. y  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph ) )
132 dfsbcq 3181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. ph  <->  [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
133132sbcbidv 3238 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
134133adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
135134adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
136129, 131, 1353bitrd 279 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ch  <->  [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
137124, 136imbi12d 320 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch )  <->  ( (
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
138115, 137rspcdv 3069 . . . . . . . . . . . . . . 15  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  ( A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch )  ->  ( ( (
# `  ( x substr  <.
0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
13950, 138rspcimdv 3067 . . . . . . . . . . . . . 14  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( A. u  e. Word  Y A. y  e. Word  X
( ( ( # `  y )  =  (
# `  u )  /\  ( # `  y
)  =  m )  ->  ch )  -> 
( ( ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
14083, 84, 114, 139syl3c 61 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph )
141140, 106jca 532 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) ) )
142 dfsbcq 3181 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  <->  [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. [. y  /  x ]. ph ) )
143 sbccom 3259 . . . . . . . . . . . . . . . 16  |-  ( [. ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. [. y  /  x ]. ph  <->  [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph )
144142, 143syl6bb 261 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  <->  [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
145117eqeq2d 2448 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( # `  y )  =  ( # `  u
)  <->  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) ) )
146144, 145anbi12d 710 . . . . . . . . . . . . . 14  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  (
# `  u )
)  <->  ( [. y  /  x ]. [. (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
147 oveq1 6093 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
u concat  <" s "> )  =  ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" s "> ) )
148147sbceq1d 3184 . . . . . . . . . . . . . 14  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. ( u concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )
)
149146, 148imbi12d 320 . . . . . . . . . . . . 13  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( ( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  ( # `  u
) )  ->  [. (
u concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )
) )
150 s1eq 12283 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  <" s ">  =  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )
151150oveq2d 6102 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" s "> )  =  ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> ) )
152151sbceq1d 3184 . . . . . . . . . . . . . . 15  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )
)
153152imbi2d 316 . . . . . . . . . . . . . 14  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. [. (
y concat  <" z "> )  /  x ]. ph ) ) )
154 sbccom 3259 . . . . . . . . . . . . . . . 16  |-  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph  <->  [. ( y concat  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph )
155154a1i 11 . . . . . . . . . . . . . . 15  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph  <->  [. ( y concat  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) )
156155imbi2d 316 . . . . . . . . . . . . . 14  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( y concat  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) ) )
157153, 156bitrd 253 . . . . . . . . . . . . 13  |-  ( s  =  ( w `  ( ( # `  w
)  -  1 ) )  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( y concat  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) ) )
158 dfsbcq 3181 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
159116eqeq1d 2445 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( # `  y )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
160158, 159anbi12d 710 . . . . . . . . . . . . . 14  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  <->  ( [. ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) ) ) )
161 oveq1 6093 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
y concat  <" z "> )  =  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" z "> ) )
162161sbceq1d 3184 . . . . . . . . . . . . . 14  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( [. ( y concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
)
163160, 162imbi12d 320 . . . . . . . . . . . . 13  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( ( [. y  /  x ]. [. (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( y concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )  <->  ( ( [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
) )
164 s1eq 12283 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( x `  ( ( # `  x
)  -  1 ) )  ->  <" z ">  =  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> )
165164oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( z  =  ( x `  ( ( # `  x
)  -  1 ) )  ->  ( (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) concat  <" z "> )  =  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> ) )
166165sbceq1d 3184 . . . . . . . . . . . . . 14  |-  ( z  =  ( x `  ( ( # `  x
)  -  1 ) )  ->  ( [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) concat  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
)
167166imbi2d 316 . . . . . . . . . . . . 13  |-  ( z  =  ( x `  ( ( # `  x
)  -  1 ) )  ->  ( (
( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )  <->  ( ( [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
) )
168 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  (
y  e. Word  X  /\  z  e.  X )
)
169 simpll 753 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  (
u  e. Word  Y  /\  s  e.  Y )
)
170 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( # `
 y )  =  ( # `  u
) )
171 wrd2ind.7 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e. Word  X  /\  z  e.  X
)  /\  ( u  e. Word  Y  /\  s  e.  Y )  /\  ( # `
 y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
172168, 169, 170, 171syl3anc 1218 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
17344ancoms 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  =  u  /\  x  =  y )  ->  ( ph  <->  ch )
)
174126, 125, 173sbc2ie 3255 . . . . . . . . . . . . . . . . 17  |-  ( [. u  /  w ]. [. y  /  x ]. ph  <->  ch )
175 ovex 6111 . . . . . . . . . . . . . . . . . 18  |-  ( u concat  <" s "> )  e.  _V
176 ovex 6111 . . . . . . . . . . . . . . . . . 18  |-  ( y concat  <" z "> )  e.  _V
177 wrd2ind.3 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  =  ( y concat  <" z "> )  /\  w  =  ( u concat  <" s "> ) )  -> 
( ph  <->  th ) )
178177ancoms 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  =  ( u concat  <" s "> )  /\  x  =  ( y concat  <" z "> ) )  -> 
( ph  <->  th ) )
179175, 176, 178sbc2ie 3255 . . . . . . . . . . . . . . . . 17  |-  ( [. ( u concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph  <->  th )
180172, 174, 1793imtr4g 270 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  ->  [. ( u concat  <" s "> )  /  w ]. [. (
y concat  <" z "> )  /  x ]. ph ) )
181180ex 434 . . . . . . . . . . . . . . 15  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( ( # `  y
)  =  ( # `  u )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  ->  [. ( u concat  <" s "> )  /  w ]. [. (
y concat  <" z "> )  /  x ]. ph ) ) )
182181com23 78 . . . . . . . . . . . . . 14  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( [. u  /  w ]. [. y  /  x ]. ph  ->  ( ( # `
 y )  =  ( # `  u
)  ->  [. ( u concat  <" s "> )  /  w ]. [. (
y concat  <" z "> )  /  x ]. ph ) ) )
183182impd 431 . . . . . . . . . . . . 13  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( ( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  ( # `  u
) )  ->  [. (
u concat  <" s "> )  /  w ]. [. ( y concat  <" z "> )  /  x ]. ph )
)
184149, 157, 163, 167, 183vtocl4ga 3035 . . . . . . . . . . . 12  |-  ( ( ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( w `  (
( # `  w )  -  1 ) )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( x `  (
( # `  x )  -  1 ) )  e.  X ) )  ->  ( ( [. ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) concat  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
)
18582, 141, 184sylc 60 . . . . . . . . . . 11  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  [. (
( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) concat  <" (
x `  ( ( # `
 x )  - 
1 ) ) "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  /  w ]. ph )
186 eqtr2 2455 . . . . . . . . . . . . . . . 16  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ( # `
 w )  =  ( m  +  1 ) )
187186ad2antll 728 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  =  ( m  +  1 ) )
188187, 90eqeltrd 2511 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  e.  NN )
189 wrdfin 12240 . . . . . . . . . . . . . . . . 17  |-  ( w  e. Word  Y  ->  w  e.  Fin )
190189adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  w  e.  Fin )
191190ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  e.  Fin )
192 hashnncl 12126 . . . . . . . . . . . . . . 15  |-  ( w  e.  Fin  ->  (
( # `  w )  e.  NN  <->  w  =/=  (/) ) )
193191, 192syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  w )  e.  NN  <->  w  =/=  (/) ) )
194188, 193mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  =/=  (/) )
195 wrdeqcats1 12360 . . . . . . . . . . . . 13  |-  ( ( w  e. Word  Y  /\  w  =/=  (/) )  ->  w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> ) )
19696, 194, 195syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> ) )
197 wrdfin 12240 . . . . . . . . . . . . . . . . 17  |-  ( x  e. Word  X  ->  x  e.  Fin )
198197adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  x  e.  Fin )
199198ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  e.  Fin )
200 hashnncl 12126 . . . . . . . . . . . . . . 15  |-  ( x  e.  Fin  ->  (
( # `  x )  e.  NN  <->  x  =/=  (/) ) )
201199, 200syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  e.  NN  <->  x  =/=  (/) ) )
20291, 201mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  =/=  (/) )
203 wrdeqcats1 12360 . . . . . . . . . . . . 13  |-  ( ( x  e. Word  X  /\  x  =/=  (/) )  ->  x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> ) )
20487, 202, 203syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> ) )
205 sbceq1a 3190 . . . . . . . . . . . . 13  |-  ( w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) concat  <" ( w `
 ( ( # `  w )  -  1 ) ) "> )  ->  ( ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) )
206 sbceq1a 3190 . . . . . . . . . . . . 13  |-  ( x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> )  ->  ( [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) )
207205, 206sylan9bb 699 . . . . . . . . . . . 12  |-  ( ( w  =  ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /\  x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> ) )  ->  ( ph 
<-> 
[. ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) )
208196, 204, 207syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( ph 
<-> 
[. ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) concat  <" ( x `
 ( ( # `  x )  -  1 ) ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) concat  <" (
w `  ( ( # `
 w )  - 
1 ) ) "> )  /  w ]. ph ) )
209185, 208mpbird 232 . . . . . . . . . 10  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ph )
210209expr 615 . . . . . . . . 9  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
w  e. Word  Y  /\  x  e. Word  X )
)  ->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) )
211210ralrimivva 2802 . . . . . . . 8  |-  ( ( m  e.  NN0  /\  A. u  e. Word  Y A. y  e. Word  X (
( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) )
212211ex 434 . . . . . . 7  |-  ( m  e.  NN0  ->  ( A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch )  ->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ph )
) )
21348, 212syl5bi 217 . . . . . 6  |-  ( m  e.  NN0  ->  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) ) )
2145, 9, 13, 17, 37, 213nn0ind 10730 . . . . 5  |-  ( (
# `  A )  e.  NN0  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
2151, 214syl 16 . . . 4  |-  ( A  e. Word  X  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
2162153ad2ant1 1009 . . 3  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
217 fveq2 5684 . . . . . . . . 9  |-  ( w  =  B  ->  ( # `
 w )  =  ( # `  B
) )
218217eqeq2d 2448 . . . . . . . 8  |-  ( w  =  B  ->  (
( # `  x )  =  ( # `  w
)  <->  ( # `  x
)  =  ( # `  B ) ) )
219218anbi1d 704 . . . . . . 7  |-  ( w  =  B  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  <->  ( ( # `
 x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) ) ) )
220 wrd2ind.5 . . . . . . 7  |-  ( w  =  B  ->  ( ph 
<->  rh ) )
221219, 220imbi12d 320 . . . . . 6  |-  ( w  =  B  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph )  <->  ( ( (
# `  x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
222221ralbidv 2729 . . . . 5  |-  ( w  =  B  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  <->  A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh ) ) )
223222rspcv 3062 . . . 4  |-  ( B  e. Word  Y  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  ->  A. x  e. Word  X
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
2242233ad2ant2 1010 . . 3  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  ->  A. x  e. Word  X
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
225216, 224mpd 15 . 2  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  A. x  e. Word  X ( ( (
# `  x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) )
226 eqidd 2438 . 2  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ( # `
 A )  =  ( # `  A
) )
227 fveq2 5684 . . . . . . . . . . 11  |-  ( x  =  A  ->  ( # `
 x )  =  ( # `  A
) )
228227eqeq1d 2445 . . . . . . . . . 10  |-  ( x  =  A  ->  (
( # `  x )  =  ( # `  B
)  <->  ( # `  A
)  =  ( # `  B ) ) )
229227eqeq1d 2445 . . . . . . . . . 10  |-  ( x  =  A  ->  (
( # `  x )  =  ( # `  A
)  <->  ( # `  A
)  =  ( # `  A ) ) )
230228, 229anbi12d 710 . . . . . . . . 9  |-  ( x  =  A  ->  (
( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  <->  ( ( # `
 A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) ) ) )
231 wrd2ind.4 . . . . . . . . 9  |-  ( x  =  A  ->  ( rh 
<->  ta ) )
232230, 231imbi12d 320 . . . . . . . 8  |-  ( x  =  A  ->  (
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh )  <->  ( ( (
# `  A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) )  ->  ta ) ) )
233232rspcv 3062 . . . . . . 7  |-  ( A  e. Word  X  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ( ( (
# `  A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) )  ->  ta ) ) )
234233com23 78 . . . . . 6  |-  ( A  e. Word  X  ->  (
( ( # `  A
)  =  ( # `  B )  /\  ( # `
 A )  =  ( # `  A
) )  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ta ) ) )
235234expd 436 . . . . 5  |-  ( A  e. Word  X  ->  (
( #