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 A1: 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 A2: 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 C1: (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 C11: (ALGO_EXGCD (p,y)) `2_3 < 0 ; :: thesis: s1 = s2

then C12: ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) by A1, C1;
ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) by A2, C1, C11;
hence s1 = s2 by C12; :: thesis: verum

end;

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

thus s1 = (ALGO_EXGCD (p,y)) `2_3 by C12, C1, A1
.= s2 by C12, C1, A2 ; :: thesis: verum

end;

end;

end;

end;

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

thus s1 = {} by A1, C2
.= s2 by A2, C2 ; :: thesis: verum

end;

end;

end;