Re: [tlaplus] library of simple finite set properties?

[Hillel Wayne <hwayne@xxxxxxxxx>]

Yup, you can find the theorems at 
https://github.com/tlaplus/v2-tlapm/tree/master/library

H

On 3/20/19 11:00 PM, David N. Jansen wrote:
> Dear all,
>
> I would like to get proofs of a few simple lemmas about IsFiniteSet and Cardinality, properties like:
>
> \A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => IsFiniteSet(S \union T)
>
> \A S: IsFiniteSet(S) => Cardinality(S) \in Nat
> \A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => Cardinality(S) <= Cardinality(T)
> \A i, j \in Int: Cardinality(i .. j) = IF i > j THEN 0 ELSE j - i
>
> I guess that someone has already proofs of these and similar properties and I don't need to redo them. I want to use them to prove correctness of an algorithm and don't want to reinvent mathematics; and while I am ok to leave some of such simple lemmas unproven, I still prefer having a proof if it already exists.
>
> Can someone of you help me? Thank you.
>
> Kind regards,
> David N. Jansen.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.