begin
theorem IdNoFix:
theorem SINCOS59ADD:
begin
:: deftheorem defines round CARDFIN2:def 1 :
theorem
theorem RoundCorrect:
begin
theorem TaylorExp:
theorem TaylorExpRest:
:: deftheorem defines derangements CARDFIN2:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
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);
:: deftheorem Def3 defines der_seq CARDFIN2:def 3 :
theorem
theorem Th7:
theorem
begin
:: deftheorem defines not-one-to-one CARDFIN2:def 4 :
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
AA:
(
F2()
= {} implies
F1()
= {} )
theorem Th8:
birthdaycomputation:
2 * ((365 |^ 23) - ((365 ! ) / ((365 -' 23) ! ))) > 365 |^ 23
theorem Th9:
theorem