let s1, s2 be Element of INT ; :: thesis: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) implies s1 = s2 )
assume A1: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) ) ; :: thesis: ( ( len nlist = 1 & not s2 = (nlist . 1) `1 ) or ( len nlist <> 1 & ( for m, n, prodc, prodi being FinSequence of INT
for M0, M being Element of INT holds
( not len m = len nlist or not len n = len nlist or not len prodc = (len nlist) - 1 or not len prodi = (len nlist) - 1 or not m . 1 = 1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for d, x, y being Element of INT holds
( not x = (nlist . i) `2 or not m . (i + 1) = (m . i) * x or not y = m . (i + 1) or not d = (nlist . (i + 1)) `2 or not prodi . i = ALGO_INVERSE (y,d) or not prodc . i = y ) ) ) or not M0 = (nlist . (len m)) `2 or not M = (prodc . ((len m) - 1)) * M0 or not n . 1 = (nlist . 1) `1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for u, u0, u1 being Element of INT holds
( not u0 = (nlist . (i + 1)) `1 or not u1 = (nlist . (i + 1)) `2 or not u = ((u0 - (n . i)) * (prodi . i)) mod u1 or not n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) ) or not s2 = (n . (len m)) mod M ) ) ) or s1 = s2 )
assume A2: ( ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) ) ; :: thesis: s1 = s2
per cases ( len nlist = 1 or len nlist <> 1 ) ;
suppose C1: len nlist = 1 ; :: thesis: s1 = s2
thus s1 = s2 by A1, A2, C1; :: thesis: verum
end;
suppose C2: len nlist <> 1 ; :: thesis: s1 = s2
consider m1, n1, prodc1, prodi1 being FinSequence of INT , M01, M1 being Element of INT such that
P1: ( len m1 = len nlist & len n1 = len nlist & len prodc1 = (len nlist) - 1 & len prodi1 = (len nlist) - 1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) ) & M01 = (nlist . (len m1)) `2 & M1 = (prodc1 . ((len m1) - 1)) * M01 & n1 . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n1 . i)) * (prodi1 . i)) mod u1 & n1 . (i + 1) = (n1 . i) + (u * (prodc1 . i)) ) ) & s1 = (n1 . (len m1)) mod M1 ) by C2, A1;
consider m2, n2, prodc2, prodi2 being FinSequence of INT , M02, M2 being Element of INT such that
P2: ( len m2 = len nlist & len n2 = len nlist & len prodc2 = (len nlist) - 1 & len prodi2 = (len nlist) - 1 & m2 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) ) & M02 = (nlist . (len m2)) `2 & M2 = (prodc2 . ((len m2) - 1)) * M02 & n2 . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n2 . i)) * (prodi2 . i)) mod u1 & n2 . (i + 1) = (n2 . i) + (u * (prodc2 . i)) ) ) & s2 = (n2 . (len m2)) mod M2 ) by C2, A2;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len m1 implies m1 . $1 = m2 . $1 );
Q50: S1[ 0 ] ;
Q51: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume Q52: S1[i] ; :: thesis: S1[i + 1]
assume ( 1 <= i + 1 & i + 1 <= len m1 ) ; :: thesis: m1 . (i + 1) = m2 . (i + 1)
then Q54: ( 1 - 1 <= (i + 1) - 1 & (i + 1) - 1 <= (len m1) - 1 ) by XREAL_1:9;
Q55: (len m1) - 1 <= (len m1) - 0 by XREAL_1:13;
per cases ( i = 0 or i <> 0 ) ;
suppose C1: i = 0 ; :: thesis: m1 . (i + 1) = m2 . (i + 1)
thus m1 . (i + 1) = m2 . (i + 1) by P1, P2, C1; :: thesis: verum
end;
suppose Q56P: i <> 0 ; :: thesis: m1 . (i + 1) = m2 . (i + 1)
then Q56: 1 <= i by NAT_1:14;
Q57: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1, Q56, Q54;
( 1 <= i & i <= (len m2) - 1 ) by Q56P, Q54, P1, P2, NAT_1:14;
then ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2;
hence m1 . (i + 1) = m2 . (i + 1) by Q57, Q54, Q52, Q55, Q56P, NAT_1:14, XXREAL_0:2; :: thesis: verum
end;
end;
end;
Q0: for k being Nat holds S1[k] from NAT_1:sch 2(Q50, Q51);
QQ3: now :: thesis: for i being Nat st 1 <= i & i <= len prodc1 holds
prodc1 . i = prodc2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len prodc1 implies prodc1 . i = prodc2 . i )
assume ASX0: ( 1 <= i & i <= len prodc1 ) ; :: thesis: prodc1 . i = prodc2 . i
then X1: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1;
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2, ASX0, P1;
hence prodc1 . i = prodc2 . i by X1, FINSEQ_1:14, P1, P2, Q0; :: thesis: verum
end;
then Q3: prodc1 = prodc2 by FINSEQ_1:14, P1, P2;
Q3A: now :: thesis: for i being Nat st 1 <= i & i <= len prodi1 holds
prodi1 . i = prodi2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len prodi1 implies prodi1 . i = prodi2 . i )
assume ASX0: ( 1 <= i & i <= len prodi1 ) ; :: thesis: prodi1 . i = prodi2 . i
then X1: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1;
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2, ASX0, P1;
hence prodi1 . i = prodi2 . i by X1, Q0, FINSEQ_1:14, P1, P2; :: thesis: verum
end;
Q4: M1 = M2 by P2, FINSEQ_1:14, P1, QQ3;
defpred S2[ Nat] means ( 1 <= $1 & $1 <= len n1 implies n1 . $1 = n2 . $1 );
Q50: S2[ 0 ] ;
Q51: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume Q52: S2[k] ; :: thesis: S2[k + 1]
assume ( 1 <= k + 1 & k + 1 <= len n1 ) ; :: thesis: n1 . (k + 1) = n2 . (k + 1)
then Q54: ( 1 - 1 <= (k + 1) - 1 & (k + 1) - 1 <= (len n1) - 1 ) by XREAL_1:9;
Q55: (len n1) - 1 <= (len n1) - 0 by XREAL_1:13;
per cases ( k = 0 or k <> 0 ) ;
suppose C1: k = 0 ; :: thesis: n1 . (k + 1) = n2 . (k + 1)
thus n1 . (k + 1) = n2 . (k + 1) by P1, P2, C1; :: thesis: verum
end;
suppose ASQ56: k <> 0 ; :: thesis: n1 . (k + 1) = n2 . (k + 1)
then Q56: 1 <= k by NAT_1:14;
Q57: ex u, u0, u1 being Element of INT st
( u0 = (nlist . (k + 1)) `1 & u1 = (nlist . (k + 1)) `2 & u = ((u0 - (n1 . k)) * (prodi1 . k)) mod u1 & n1 . (k + 1) = (n1 . k) + (u * (prodc1 . k)) ) by Q56, Q54, P1;
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (k + 1)) `1 & u1 = (nlist . (k + 1)) `2 & u = ((u0 - (n2 . k)) * (prodi2 . k)) mod u1 & n2 . (k + 1) = (n2 . k) + (u * (prodc2 . k)) ) by Q56, Q54, P1, P2;
hence n1 . (k + 1) = n2 . (k + 1) by Q3, Q57, Q52, Q55, ASQ56, NAT_1:14, Q54, XXREAL_0:2, FINSEQ_1:14, P1, P2, Q3A; :: thesis: verum
end;
end;
end;
for k being Nat holds S2[k] from NAT_1:sch 2(Q50, Q51);
hence s1 = s2 by Q4, P1, P2, FINSEQ_1:14; :: thesis: verum
end;
end;