let s1, s2 be Element of INT ; :: thesis: ( ( for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) implies s1 = s2 )

assume A6: for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ; :: thesis: ( ex y being Element of INT st

( y = x mod p & not ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) or s1 = s2 )

assume A7: for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ; :: thesis: s1 = s2

reconsider y = x mod p as Element of INT by INT_1:def 2;

thus s1 = s2 :: thesis: verum

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) implies s1 = s2 )

assume A6: for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ; :: thesis: ( ex y being Element of INT st

( y = x mod p & not ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) or s1 = s2 )

assume A7: for y being Element of INT st y = x mod p holds

( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ; :: thesis: s1 = s2

reconsider y = x mod p as Element of INT by INT_1:def 2;

thus s1 = s2 :: thesis: verum

proof
end;

per cases
( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 )
;

end;

suppose A8:
(ALGO_EXGCD (p,y)) `3_3 = 1
; :: thesis: s1 = s2

thus
s1 = s2
:: thesis: verum

end;proof
end;

per cases
( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 )
;

end;

suppose A9:
(ALGO_EXGCD (p,y)) `2_3 < 0
; :: thesis: s1 = s2

then A10:
ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) by A6, A8;

ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) by A7, A8, A9;

hence s1 = s2 by A10; :: thesis: verum

end;( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) by A6, A8;

ex z being Element of INT st

( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) by A7, A8, A9;

hence s1 = s2 by A10; :: thesis: verum