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

proof

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

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

thus s1 = s2 :: thesis: verum

proof

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

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;

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

hence s1 = (ALGO_EXGCD (p,y)) `2_3 by A8, A6
.= s2 by A11, A8, A7 ;
:: thesis: verum

end;

end;

end;

end;

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

hence s1 = {} by A6
.= s2 by A7, A12 ;
:: thesis: verum

end;

end;

end;