# [isabelle] new in the AFP: A formal proof of the max-flow min-cut theorem for countable networks

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] new in the AFP: A formal proof of the max-flow min-cut theorem for countable networks
*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>
*Date*: Mon, 9 May 2016 00:52:09 +0000
*Accept-language*: en-AU, en-US
*Thread-index*: AQHRqY0Ekhm/g5Z2+0iK76o7cbaomQ==
*Thread-topic*: new in the AFP: A formal proof of the max-flow min-cut theorem for countable networks

Another new entry in the Archive, keep them coming!
A formal proof of the max-flow min-cut theorem for countable networks
by Andreas Lochbihler
This article formalises a proof of the maximum-flow minimal-cut theorem for networks with countably many edges. A network is a directed graph with non-negative real-valued edge labels and two dedicated vertices, the source and the sink. A flow in a network assigns non-negative real numbers to the edges such that for all vertices except for the source and the sink, the sum of values on incoming edges equals the sum of values on outgoing edges. A cut is a subset of the vertices which contains the source, but not the sink. Our theorem states that in every network, there is a flow and a cut such that the flow saturates all the edges going out of the cut and is zero on all the incoming edges. The proof is based on the paper The Max-Flow Min-Cut theorem for countable networksby Aharoni et al. As an application, we derive a characterisation of the lifting operation for relations on discrete probability distributions, which leads to a concise proof of its distributivity over relation composition.
http://www.isa-afp.org/entries/MFMC_Countable.shtml
Enjoy!
Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*