let t1, t2 be Integer; :: thesis: ( ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t1 = pn . 1 ) ) ) ) & ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t2 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t2 = pn . 1 ) ) ) ) implies t1 = t2 )
assume that
A109: ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t1 = pn . 1 ) ) ) ) and
A110: ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t2 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t2 = pn . 1 ) ) ) ) ; :: thesis: t1 = t2
consider sm1, sn1, pn1 being FinSequence of INT such that
len sm1 = n + 1 and
len sn1 = n + 1 and
len pn1 = n + 1 and
A111: ( n < m implies t1 = 0 ) and
A112: ( not n < m implies ( sm1 . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm1 . (k + 1) = (sm1 . k) * 2 & not sm1 . (k + 1) > n ) ) & sm1 . (i + 1) = (sm1 . i) * 2 & sm1 . (i + 1) > n & pn1 . (i + 1) = 0 & sn1 . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn1 . ((i + 1) - (j - 1)) >= sm1 . ((i + 1) - j) implies ( sn1 . ((i + 1) - j) = (sn1 . ((i + 1) - (j - 1))) - (sm1 . ((i + 1) - j)) & pn1 . ((i + 1) - j) = ((pn1 . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn1 . ((i + 1) - (j - 1)) >= sm1 . ((i + 1) - j) implies ( sn1 . ((i + 1) - j) = sn1 . ((i + 1) - (j - 1)) & pn1 . ((i + 1) - j) = (pn1 . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t1 = pn1 . 1 ) ) ) by A109;
consider sm2, sn2, pn2 being FinSequence of INT such that
len sm2 = n + 1 and
len sn2 = n + 1 and
len pn2 = n + 1 and
A113: ( n < m implies t2 = 0 ) and
A114: ( not n < m implies ( sm2 . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm2 . (k + 1) = (sm2 . k) * 2 & not sm2 . (k + 1) > n ) ) & sm2 . (i + 1) = (sm2 . i) * 2 & sm2 . (i + 1) > n & pn2 . (i + 1) = 0 & sn2 . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn2 . ((i + 1) - (j - 1)) >= sm2 . ((i + 1) - j) implies ( sn2 . ((i + 1) - j) = (sn2 . ((i + 1) - (j - 1))) - (sm2 . ((i + 1) - j)) & pn2 . ((i + 1) - j) = ((pn2 . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn2 . ((i + 1) - (j - 1)) >= sm2 . ((i + 1) - j) implies ( sn2 . ((i + 1) - j) = sn2 . ((i + 1) - (j - 1)) & pn2 . ((i + 1) - j) = (pn2 . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t2 = pn2 . 1 ) ) ) by A110;
now :: thesis: t1 = t2
per cases ( n < m or n >= m ) ;
suppose n < m ; :: thesis: t1 = t2
hence t1 = t2 by A111, A113; :: thesis: verum
end;
suppose A115: n >= m ; :: thesis: t1 = t2
then consider i1 being Integer such that
A116: 1 <= i1 and
i1 <= n and
A117: for k being Integer st 1 <= k & k < i1 holds
( sm1 . (k + 1) = (sm1 . k) * 2 & not sm1 . (k + 1) > n ) and
A118: sm1 . (i1 + 1) = (sm1 . i1) * 2 and
A119: sm1 . (i1 + 1) > n and
A120: pn1 . (i1 + 1) = 0 and
A121: sn1 . (i1 + 1) = n and
A122: for j being Integer st 1 <= j & j <= i1 holds
( ( sn1 . ((i1 + 1) - (j - 1)) >= sm1 . ((i1 + 1) - j) implies ( sn1 . ((i1 + 1) - j) = (sn1 . ((i1 + 1) - (j - 1))) - (sm1 . ((i1 + 1) - j)) & pn1 . ((i1 + 1) - j) = ((pn1 . ((i1 + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn1 . ((i1 + 1) - (j - 1)) >= sm1 . ((i1 + 1) - j) implies ( sn1 . ((i1 + 1) - j) = sn1 . ((i1 + 1) - (j - 1)) & pn1 . ((i1 + 1) - j) = (pn1 . ((i1 + 1) - (j - 1))) * 2 ) ) ) and
A123: t1 = pn1 . 1 by A112;
reconsider ii1 = i1 as Element of NAT by A116, INT_1:3;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= i1 + 1 implies sm1 . $1 = sm2 . $1 );
defpred S2[ Nat] means ( 1 <= $1 & $1 <= i1 + 1 implies pn1 . (((ii1 + 1) + 1) -' $1) = pn2 . (((ii1 + 1) + 1) -' $1) );
defpred S3[ Nat] means ( 1 <= $1 & $1 <= i1 + 1 implies sn1 . (((ii1 + 1) + 1) -' $1) = sn2 . (((ii1 + 1) + 1) -' $1) );
consider i2 being Integer such that
A124: 1 <= i2 and
i2 <= n and
A125: for k being Integer st 1 <= k & k < i2 holds
( sm2 . (k + 1) = (sm2 . k) * 2 & not sm2 . (k + 1) > n ) and
A126: sm2 . (i2 + 1) = (sm2 . i2) * 2 and
A127: sm2 . (i2 + 1) > n and
A128: pn2 . (i2 + 1) = 0 and
A129: sn2 . (i2 + 1) = n and
A130: for j being Integer st 1 <= j & j <= i2 holds
( ( sn2 . ((i2 + 1) - (j - 1)) >= sm2 . ((i2 + 1) - j) implies ( sn2 . ((i2 + 1) - j) = (sn2 . ((i2 + 1) - (j - 1))) - (sm2 . ((i2 + 1) - j)) & pn2 . ((i2 + 1) - j) = ((pn2 . ((i2 + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn2 . ((i2 + 1) - (j - 1)) >= sm2 . ((i2 + 1) - j) implies ( sn2 . ((i2 + 1) - j) = sn2 . ((i2 + 1) - (j - 1)) & pn2 . ((i2 + 1) - j) = (pn2 . ((i2 + 1) - (j - 1))) * 2 ) ) ) and
A131: t2 = pn2 . 1 by A114, A115;
reconsider ii2 = i2 as Element of NAT by A124, INT_1:3;
A132: now :: thesis: not i2 < i1
assume A133: i2 < i1 ; :: thesis: contradiction
A134: for k being Integer st 1 <= k & k <= i2 + 1 holds
sm2 . k = sm1 . k
proof
defpred S4[ Nat] means ( $1 < i2 + 1 implies sm2 . ($1 + 1) = sm1 . ($1 + 1) );
let k be Integer; :: thesis: ( 1 <= k & k <= i2 + 1 implies sm2 . k = sm1 . k )
assume that
A135: 1 <= k and
A136: k <= i2 + 1 ; :: thesis: sm2 . k = sm1 . k
reconsider kh = k as Element of NAT by A135, INT_1:3;
k - 1 >= 0 by A135, XREAL_1:48;
then A137: kh -' 1 = k - 1 by XREAL_0:def 2;
then A138: (kh -' 1) + 1 = k ;
A139: for e being Nat st S4[e] holds
S4[e + 1]
proof
let e be Nat; :: thesis: ( S4[e] implies S4[e + 1] )
assume A140: S4[e] ; :: thesis: S4[e + 1]
per cases ( e + 1 < i2 + 1 or e + 1 >= i2 + 1 ) ;
suppose e + 1 < i2 + 1 ; :: thesis: S4[e + 1]
then (e + 1) + 1 <= ii2 + 1 by NAT_1:13;
then A141: ((e + 1) + 1) - 1 <= (i2 + 1) - 1 by XREAL_1:9;
A142: 0 + 1 <= e + 1 by XREAL_1:7;
A143: now :: thesis: ( ( e + 1 < i2 & sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 ) or ( e + 1 >= i2 & sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 ) )
per cases ( e + 1 < i2 or e + 1 >= i2 ) ;
case e + 1 < i2 ; :: thesis: sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2
hence sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 by A125, A142; :: thesis: verum
end;
case e + 1 >= i2 ; :: thesis: sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2
then e + 1 = i2 by A141, XXREAL_0:1;
hence sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 by A126; :: thesis: verum
end;
end;
end;
A144: e < e + 1 by NAT_1:13;
e + 1 < i1 by A133, A141, XXREAL_0:2;
hence S4[e + 1] by A117, A140, A142, A144, A143, XXREAL_0:2; :: thesis: verum
end;
suppose e + 1 >= i2 + 1 ; :: thesis: S4[e + 1]
hence S4[e + 1] ; :: thesis: verum
end;
end;
end;
A145: S4[ 0 ] by A112, A114, A115;
A146: for e being Nat holds S4[e] from NAT_1:sch 2(A145, A139);
 A147: ii2 < ii2 + 1 by NAT_1:13;
k - 1 <= (i2 + 1) - 1 by A136, XREAL_1:9;
then kh -' 1 < i2 + 1 by A137, A147, XXREAL_0:2;
hence sm2 . k = sm1 . k by A138, A146; :: thesis: verum
end;
0 <= ii2 ;
then 0 + 1 <= i2 + 1 by XREAL_1:7;
then sm2 . (i2 + 1) = sm1 . (i2 + 1) by A134;
hence contradiction by A117, A124, A127, A133; :: thesis: verum
end;
A148: now :: thesis: not i1 < i2
assume A149: i1 < i2 ; :: thesis: contradiction
A150: for k being Integer st 1 <= k & k <= i1 + 1 holds
sm1 . k = sm2 . k
proof
defpred S4[ Nat] means ( $1 < i1 + 1 implies sm1 . ($1 + 1) = sm2 . ($1 + 1) );
let k be Integer; :: thesis: ( 1 <= k & k <= i1 + 1 implies sm1 . k = sm2 . k )
assume that
A151: 1 <= k and
A152: k <= i1 + 1 ; :: thesis: sm1 . k = sm2 . k
reconsider kh = k as Element of NAT by A151, INT_1:3;
k - 1 >= 0 by A151, XREAL_1:48;
then A153: kh -' 1 = k - 1 by XREAL_0:def 2;
then A154: (kh -' 1) + 1 = k ;
A155: for e being Nat st S4[e] holds
S4[e + 1]
proof
let e be Nat; :: thesis: ( S4[e] implies S4[e + 1] )
assume A156: S4[e] ; :: thesis: S4[e + 1]
per cases ( e + 1 < i1 + 1 or e + 1 >= i1 + 1 ) ;
suppose e + 1 < i1 + 1 ; :: thesis: S4[e + 1]
then (e + 1) + 1 <= ii1 + 1 by NAT_1:13;
then A157: ((e + 1) + 1) - 1 <= (i1 + 1) - 1 by XREAL_1:9;
A158: 0 + 1 <= e + 1 by XREAL_1:7;
A159: now :: thesis: ( ( e + 1 < i1 & sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 ) or ( e + 1 >= i1 & sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 ) )
per cases ( e + 1 < i1 or e + 1 >= i1 ) ;
case e + 1 < i1 ; :: thesis: sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2
hence sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 by A117, A158; :: thesis: verum
end;
case e + 1 >= i1 ; :: thesis: sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2
then e + 1 = i1 by A157, XXREAL_0:1;
hence sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 by A118; :: thesis: verum
end;
end;
end;
A160: e < e + 1 by NAT_1:13;
e + 1 < i2 by A149, A157, XXREAL_0:2;
hence S4[e + 1] by A125, A156, A158, A160, A159, XXREAL_0:2; :: thesis: verum
end;
suppose e + 1 >= i1 + 1 ; :: thesis: S4[e + 1]
hence S4[e + 1] ; :: thesis: verum
end;
end;
end;
A161: S4[ 0 ] by A112, A114, A115;
A162: for e being Nat holds S4[e] from NAT_1:sch 2(A161, A155);
 A163: ii1 < ii1 + 1 by NAT_1:13;
k - 1 <= (i1 + 1) - 1 by A152, XREAL_1:9;
then kh -' 1 < i1 + 1 by A153, A163, XXREAL_0:2;
hence sm1 . k = sm2 . k by A154, A162; :: thesis: verum
end;
0 <= ii1 ;
then 0 + 1 <= i1 + 1 by XREAL_1:7;
then sm1 . (i1 + 1) = sm2 . (i1 + 1) by A150;
hence contradiction by A116, A119, A125, A149; :: thesis: verum
end;
then A164: i1 = i2 by A132, XXREAL_0:1;
A165: ii1 < ii1 + 1 by NAT_1:13;
A166: for kk being Nat st S1[kk] holds
S1[kk + 1]
proof
let kk be Nat; :: thesis: ( S1[kk] implies S1[kk + 1] )
assume A167: S1[kk] ; :: thesis: S1[kk + 1]
( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies sm1 . (kk + 1) = sm2 . (kk + 1) )
proof
assume that
1 <= kk + 1 and
A168: kk + 1 <= i1 + 1 ; :: thesis: sm1 . (kk + 1) = sm2 . (kk + 1)
per cases ( kk + 1 < i1 + 1 or kk + 1 = i1 + 1 ) by A168, XXREAL_0:1;
suppose A169: kk + 1 < i1 + 1 ; :: thesis: sm1 . (kk + 1) = sm2 . (kk + 1)
then A170: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, XREAL_1:9;
now :: thesis: ( ( 0 < kk & sm1 . (kk + 1) = sm2 . (kk + 1) ) or ( 0 >= kk & sm1 . (kk + 1) = sm2 . (kk + 1) ) )
per cases ( 0 < kk or 0 >= kk ) ;
case 0 < kk ; :: thesis: sm1 . (kk + 1) = sm2 . (kk + 1)
then A171: 0 + 1 <= kk by NAT_1:13;
A172: now :: thesis: ( ( kk < i2 & sm2 . (kk + 1) = (sm2 . kk) * 2 ) or ( kk >= i2 & sm2 . (kk + 1) = (sm2 . kk) * 2 ) )
per cases ( kk < i2 or kk >= i2 ) ;
case kk < i2 ; :: thesis: sm2 . (kk + 1) = (sm2 . kk) * 2
hence sm2 . (kk + 1) = (sm2 . kk) * 2 by A125, A171; :: thesis: verum
end;
case kk >= i2 ; :: thesis: sm2 . (kk + 1) = (sm2 . kk) * 2
then kk = i2 by A170, XXREAL_0:1;
hence sm2 . (kk + 1) = (sm2 . kk) * 2 by A126; :: thesis: verum
end;
end;
end;
kk < i1 by A169, XREAL_1:7;
hence sm1 . (kk + 1) = sm2 . (kk + 1) by A117, A165, A167, A171, A172, XXREAL_0:2; :: thesis: verum
end;
case 0 >= kk ; :: thesis: sm1 . (kk + 1) = sm2 . (kk + 1)
then kk = 0 ;
hence sm1 . (kk + 1) = sm2 . (kk + 1) by A112, A114, A115; :: thesis: verum
end;
end;
end;
hence sm1 . (kk + 1) = sm2 . (kk + 1) ; :: thesis: verum
end;
suppose kk + 1 = i1 + 1 ; :: thesis: sm1 . (kk + 1) = sm2 . (kk + 1)
hence sm1 . (kk + 1) = sm2 . (kk + 1) by A116, A118, A126, A164, A167, NAT_1:13; :: thesis: verum
end;
end;
end;
hence S1[kk + 1] ; :: thesis: verum
end;
A173: S1[ 0 ] ;
A174: for jj being Nat holds S1[jj] from NAT_1:sch 2(A173, A166);
A175: for jj being Integer st 1 <= jj & jj <= i1 + 1 holds
sm1 . jj = sm2 . jj
proof
let jj be Integer; :: thesis: ( 1 <= jj & jj <= i1 + 1 implies sm1 . jj = sm2 . jj )
assume that
A176: 1 <= jj and
A177: jj <= i1 + 1 ; :: thesis: sm1 . jj = sm2 . jj
reconsider jj2 = jj as Element of NAT by A176, INT_1:3;
sm1 . jj2 = sm2 . jj2 by A174, A176, A177;
hence sm1 . jj = sm2 . jj ; :: thesis: verum
end;
A178: for kk being Nat st S3[kk] holds
S3[kk + 1]
proof
let kk be Nat; :: thesis: ( S3[kk] implies S3[kk + 1] )
assume A179: S3[kk] ; :: thesis: S3[kk + 1]
( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) )
proof
assume that
1 <= kk + 1 and
A180: kk + 1 <= i1 + 1 ; :: thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1))
A181: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, A180, XREAL_1:9;
per cases ( 0 < kk or 0 >= kk ) ;
suppose A182: 0 < kk ; :: thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1))
A183: kk < i1 + 1 by A164, A165, A181, XXREAL_0:2;
then (i1 + 1) - kk > 0 by XREAL_1:50;
then A184: (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def 2;
A185: 0 + 1 <= kk by A182, NAT_1:13;
then A186: kk - 1 >= 0 by XREAL_1:48;
kk -' 1 <= kk by NAT_D:35;
then kk -' 1 < i1 + 1 by A183, XXREAL_0:2;
then (i1 + 1) - (kk -' 1) >= 0 by XREAL_1:48;
then A187: (ii1 + 1) -' (kk -' 1) = (i1 + 1) - (kk -' 1) by XREAL_0:def 2
.= (i1 + 1) - (kk - 1) by A186, XREAL_0:def 2 ;
now :: thesis: ( ( kk <= i2 & sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) ) or ( kk > i2 & contradiction ) )
per cases ( kk <= i2 or kk > i2 ) ;
case A188: kk <= i2 ; :: thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1))
ii1 < ii1 + 1 by NAT_1:13;
then kk < i1 + 1 by A164, A188, XXREAL_0:2;
then A189: (i1 + 1) - kk > 0 by XREAL_1:50;
then (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def 2;
then A190: (ii1 + 1) -' kk >= 0 + 1 by A189, NAT_1:13;
A191: ( (ii1 + 1) -' kk <= i1 + 1 & ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk ) by Th1, NAT_D:35;
A192: ( not sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = sn2 . ((ii1 + 1) -' (kk -' 1)) & pn2 . ((ii1 + 1) -' kk) = (pn2 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A130, A164, A185, A187, A184, A188;
kk - 1 >= 0 by A185, XREAL_1:48;
then kk -' 1 = kk - 1 by XREAL_0:def 2;
then kk = (kk -' 1) + 1 ;
then A193: ((ii1 + 1) + 1) -' kk = (ii1 + 1) -' (kk -' 1) by Th1;
A194: ( sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = (sn2 . ((ii1 + 1) -' (kk -' 1))) - (sm2 . ((ii1 + 1) -' kk)) & pn2 . ((ii1 + 1) -' kk) = ((pn2 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A130, A164, A185, A187, A184, A188;
A195: ( not sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = sn1 . ((ii1 + 1) -' (kk -' 1)) & pn1 . ((ii1 + 1) -' kk) = (pn1 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A122, A164, A185, A187, A184, A188;
( sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = (sn1 . ((ii1 + 1) -' (kk -' 1))) - (sm1 . ((ii1 + 1) -' kk)) & pn1 . ((ii1 + 1) -' kk) = ((pn1 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A122, A164, A185, A187, A184, A188;
hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A164, A175, A179, A182, A188, A195, A194, A192, A190, A193, A191, NAT_1:13; :: thesis: verum
end;
end;
end;
hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) ; :: thesis: verum
end;
suppose 0 >= kk ; :: thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1))
then A196: kk = 0 ;
((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1
.= ii1 + 1 by A196, NAT_D:40 ;
hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A121, A129, A148, A132, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence S3[kk + 1] ; :: thesis: verum
end;
A197: S3[ 0 ] ;
A198: for jj being Nat holds S3[jj] from NAT_1:sch 2(A197, A178);
A199: for kk being Nat st S2[kk] holds
S2[kk + 1]
proof
let kk be Nat; :: thesis: ( S2[kk] implies S2[kk + 1] )
assume A200: S2[kk] ; :: thesis: S2[kk + 1]
( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) )
proof
assume that
1 <= kk + 1 and
A201: kk + 1 <= i1 + 1 ; :: thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1))
A202: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, A201, XREAL_1:9;
per cases ( 0 < kk or 0 >= kk ) ;
suppose A203: 0 < kk ; :: thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1))
A204: kk -' 1 < (kk -' 1) + 1 by NAT_1:13;
kk < ii1 + 1 by A201, NAT_1:13;
then (i1 + 1) - kk > 0 by XREAL_1:50;
then A205: (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def 2;
A206: 0 + 1 <= kk by A203, NAT_1:13;
then A207: kk - 1 >= 0 by XREAL_1:48;
then kk - 1 = kk -' 1 by XREAL_0:def 2;
then kk -' 1 < i2 by A202, A204, XXREAL_0:2;
then kk -' 1 < i2 + 1 by A164, A165, XXREAL_0:2;
then (i1 + 1) - (kk -' 1) >= 0 by A164, XREAL_1:48;
then A208: (ii1 + 1) -' (kk -' 1) = (i1 + 1) - (kk -' 1) by XREAL_0:def 2
.= (i1 + 1) - (kk - 1) by A207, XREAL_0:def 2 ;
now :: thesis: ( ( kk <= i2 & pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) ) or ( kk > i2 & contradiction ) )
per cases ( kk <= i2 or kk > i2 ) ;
case A209: kk <= i2 ; :: thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1))
ii1 < ii1 + 1 by NAT_1:13;
then A210: kk < i1 + 1 by A164, A209, XXREAL_0:2;
then A211: (i1 + 1) - kk > 0 by XREAL_1:50;
then (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def 2;
then (ii1 + 1) -' kk >= 0 + 1 by A211, NAT_1:13;
then A212: sm1 . ((ii1 + 1) -' kk) = sm2 . ((ii1 + 1) -' kk) by A175, NAT_D:35;
kk - 1 >= 0 by A206, XREAL_1:48;
then kk -' 1 = kk - 1 by XREAL_0:def 2;
then kk = (kk -' 1) + 1 ;
then A213: ((ii1 + 1) + 1) -' kk = (ii1 + 1) -' (kk -' 1) by Th1;
A214: ( not sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = sn1 . ((ii1 + 1) -' (kk -' 1)) & pn1 . ((ii1 + 1) -' kk) = (pn1 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A122, A164, A206, A208, A205, A209;
A215: ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1;
A216: ( not sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = sn2 . ((ii1 + 1) -' (kk -' 1)) & pn2 . ((ii1 + 1) -' kk) = (pn2 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A130, A164, A206, A208, A205, A209;
A217: ( sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = (sn2 . ((ii1 + 1) -' (kk -' 1))) - (sm2 . ((ii1 + 1) -' kk)) & pn2 . ((ii1 + 1) -' kk) = ((pn2 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A130, A164, A206, A208, A205, A209;
( sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = (sn1 . ((ii1 + 1) -' (kk -' 1))) - (sm1 . ((ii1 + 1) -' kk)) & pn1 . ((ii1 + 1) -' kk) = ((pn1 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A122, A164, A206, A208, A205, A209;
hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A198, A200, A206, A214, A217, A216, A210, A213, A212, A215; :: thesis: verum
end;
end;
end;
hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) ; :: thesis: verum
end;
suppose 0 >= kk ; :: thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1))
then A218: kk = 0 ;
((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1
.= i1 + 1 by A218, NAT_D:40 ;
hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A120, A128, A148, A132, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence S2[kk + 1] ; :: thesis: verum
end;
A219: S2[ 0 ] ;
A220: for jj being Nat holds S2[jj] from NAT_1:sch 2(A219, A199);
A221: for jj being Integer st 1 <= jj & jj <= i1 + 1 holds
pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj)
proof
let jj be Integer; :: thesis: ( 1 <= jj & jj <= i1 + 1 implies pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) )
assume that
A222: 1 <= jj and
A223: jj <= i1 + 1 ; :: thesis: pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj)
reconsider j2 = jj as Element of NAT by A222, INT_1:3;
ii1 + 1 < (ii1 + 1) + 1 by NAT_1:13;
then jj < (ii1 + 1) + 1 by A223, XXREAL_0:2;
then ((ii1 + 1) + 1) - j2 >= 0 by XREAL_1:48;
then ((ii1 + 1) + 1) -' j2 = ((ii1 + 1) + 1) - jj by XREAL_0:def 2;
hence pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) by A220, A222, A223; :: thesis: verum
end;
( 1 <= 1 + ii1 & ((i1 + 1) + 1) - (i1 + 1) = 1 ) by NAT_1:11;
hence t1 = t2 by A123, A131, A221; :: thesis: verum
end;
end;
end;
hence t1 = t2 ; :: thesis: verum