--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
THEOREM ax1 == ASSUME NEW x \in Int PROVE IsFiniteSet({x})
THEOREM ax2 == ASSUME NEW x \in Int, NEW y \in Int PROVE IsFiniteSet({y-x})
THEOREM ax3 == ASSUME NEW S1, NEW S2,
/\ IsFiniteSet(S1)
/\ IsFiniteSet(S2)
PROVE /\ IsFiniteSet(S1 \ S2)
/\ IsFiniteSet(S1 \cup S2)
THEOREM Spec => []PartialCorrectness
<1>1. Init => SInv
BY InputOK DEF Init, SInv, TypeOK, PartialCorrectness
<1>2. SInv /\ [Next]_vars => SInv'
<2> SUFFICES ASSUME SInv /\ [Next]_vars
PROVE SInv'
OBVIOUS
<2>1. TypeOK'
<3>1. CASE Lbl_1
<4>1. (S \subseteq Nat \{0})'
BY <3>1 DEF SInv, TypeOK, Next, vars, Lbl_1
<4>2. (S # {})'
BY <3>1 DEF SetGCD, SInv, TypeOK, Next, vars, Lbl_1, SetMax, Divides
<4>3. IsFiniteSet(S)'
BY <3>1, ax1, ax2, ax3 DEF SInv, TypeOK, Next, vars, Lbl_1
<4>4. QED
BY <4>1, <4>2, <4>3 DEF TypeOK
<3>2. CASE pc = "Done" /\ UNCHANGED vars
BY <3>2 DEF PartialCorrectness, SInv, TypeOK, vars
<3>3. CASE UNCHANGED vars
BY <3>3 DEF Init, SetGCD, PartialCorrectness, SInv, TypeOK, Next, vars
<3>4. QED
BY <3>1, <3>2, <3>3 DEF Next
<2>2. (SetGCD(S) = SetGCD(T))'
BY InputOK DEF Init, SInv, TypeOK, Next, vars
<2>3. PartialCorrectness'
BY InputOK DEF Init, SInv, TypeOK, Next, vars
<2>4. QED
BY <2>1, <2>2, <2>3 DEF SInv
<1>3. SInv => PartialCorrectness
BY DEF SInv, PartialCorrectness
<1>4. QED
BY <1>1, <1>2, <1>3, PTL DEF Spec
Yes, I initially just added ax1 and ax3 (then called “ax2”) for my proof – but when that didn’t work (and I hadn’t any other idea as to why not) I added the additional axiom (ax2), despite feeling that it shouldn’t be needed.
(I am new to TLAPS – so I am still learning the ropes.)
I have attached the module.
By the way, your suggestion of using FS_AddElement and FS_RemoveElement worked.
Thanks
Jens
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/c9kjW0Hv6Dc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
<SetEuclid.tla>