[tlaplus] library of simple finite set properties?

["David N. Jansen" <dnjansen@xxxxxxxxx>]

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.