begin
begin
begin
reconsider j = 1, z = 0 as Element of INT by INT_1:def 2;
deffunc H1( Element of NAT , Integer, Integer) -> Element of INT = ($1 + 1) * ($2 + $3);
begin
scheme
FraenkelDiff{
F1()
-> set ,
F2()
-> set ,
P1[
set ] } :
{ f where f is Function of F1(),F2() : P1[f] } = (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
provided
A1:
(
F2()
= {} implies
F1()
= {} )
Lm1:
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
:: we cannot divide and it has to be proved separately.