Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Discrete Summation


view this post on Zulip Email Gateway (Aug 19 2022 at 14:18):

From: Tobias Nipkow <nipkow@in.tum.de>
Discrete Summation
Florian Haftmann with contributions by Amine Chaieb

These theories introduce basic concepts and proofs about discrete summation:
shifts, formal summation, falling factorials and stirling numbers. As proof of
concept, a simple summation conversion is provided.

http://afp.sourceforge.net/entries/Discrete_Summation.shtml

Enjoy!


Last updated: Nov 21 2024 at 12:39 UTC