defpred S1[ Integer] means ( ( m = 0 implies n div m = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies n div m = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( $1 = idiv1_prg (n,(- m)) & ( (- m) * $1 = n implies n div m = - $1 ) & ( (- m) * $1 <> n implies n div m = (- $1) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( $1 = idiv1_prg ((- n),m) & ( m * $1 = - n implies n div m = - $1 ) & ( m * $1 <> - n implies n div m = (- $1) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies n div m = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) );
per cases
( m = 0 or m <> 0 )
;
suppose
m = 0
;
ex b1, i being Integer st
( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) )hence
ex
b1,
i being
Integer st
( (
m = 0 implies
b1 = 0 ) & ( not
m = 0 implies ( (
n >= 0 &
m > 0 implies
b1 = idiv1_prg (
n,
m) ) & ( ( not
n >= 0 or not
m > 0 ) implies ( (
n >= 0 &
m < 0 implies (
i = idiv1_prg (
n,
(- m)) & (
(- m) * i = n implies
b1 = - i ) & (
(- m) * i <> n implies
b1 = (- i) - 1 ) ) ) & ( ( not
n >= 0 or not
m < 0 ) implies ( (
n < 0 &
m > 0 implies (
i = idiv1_prg (
(- n),
m) & (
m * i = - n implies
b1 = - i ) & (
m * i <> - n implies
b1 = (- i) - 1 ) ) ) & ( ( not
n < 0 or not
m > 0 ) implies
b1 = idiv1_prg (
(- n),
(- m)) ) ) ) ) ) ) ) )
;
verum end; suppose A1:
m <> 0
;
ex b1, i being Integer st
( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) )hence
ex
b1,
i being
Integer st
( (
m = 0 implies
b1 = 0 ) & ( not
m = 0 implies ( (
n >= 0 &
m > 0 implies
b1 = idiv1_prg (
n,
m) ) & ( ( not
n >= 0 or not
m > 0 ) implies ( (
n >= 0 &
m < 0 implies (
i = idiv1_prg (
n,
(- m)) & (
(- m) * i = n implies
b1 = - i ) & (
(- m) * i <> n implies
b1 = (- i) - 1 ) ) ) & ( ( not
n >= 0 or not
m < 0 ) implies ( (
n < 0 &
m > 0 implies (
i = idiv1_prg (
(- n),
m) & (
m * i = - n implies
b1 = - i ) & (
m * i <> - n implies
b1 = (- i) - 1 ) ) ) & ( ( not
n < 0 or not
m > 0 ) implies
b1 = idiv1_prg (
(- n),
(- m)) ) ) ) ) ) ) ) )
;
verum end; end;