[
Date Prev
][
Date Next
][
Thread Prev
][
Thread Next
][
Date Index
][
Thread Index
]
Missing theorem
From
: fl <
freder...@xxxxxxxxxxx
>
Date
: Fri, 7 Nov 2014 06:50:49 -0800 (PST)
A theorem that is missing in SequenceProperties. tla (in my opinion).
ASSUME NEW S, NEW J \in Nat, NEW seq \in [ 1 .. J -> S ]
PROVE seq \in Seq(S)
--
FL
Follow-Ups
:
Re: Missing theorem
From:
Leslie Lamport
Re: [tlaplus] Missing theorem
From:
Stephan Merz
Prev by Date:
Re: Proofs of integer properties
Next by Date:
Re: [tlaplus] Missing theorem
Previous by thread:
Re: Proofs of integer properties
Next by thread:
Re: [tlaplus] Missing theorem
Index(es):
Date
Thread