[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] library of simple finite set properties?
- From: "David N. Jansen" <dnjansen@xxxxxxxxx>
- Date: Thu, 21 Mar 2019 04:00:27 +0000
- Accept-language: nl-NL, zh-CN, en-US
- Thread-index: AQHU35qeILzKu6CfzEeAhj4/navGMQ==
- Thread-topic: library of simple finite set properties?
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.
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.