[tlaplus] The CASE keyword

Hi,

In the example of hierarchical proofs in the TLAPS tutorial (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html), the two possible actions of Next are considered in the proof using the CASE keyword:

Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = y

THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'

<1> SUFFICES ASSUME InductiveInvariant, Next PROVE InductiveInvariant' <1> USE DEF InductiveInvariant, Next <1>1 (x < y) \/ (y < x) <1>a CASE x < y <1>b CASE y < x <1>2 QED BY <1>1, <1>a, <1>b

It is quite intuitive because this can be read as "the two separate cases that can occur in the next step.".

However, in the proof for Paxos (https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla), in the proof of the intermediate Lemma SafeAtStable, the different cases that can happen in the next state are expressed by using ASSUME keyword:

Next == \/ \E b \in Ballots : Phase1a(b) \/ Phase2a(b)
	\/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)

LEMMA SafeAtStable == Inv /\ Next /\ TypeOK' =>
	\A v \in Values, b \in Ballots:
	SafeAt(v, b) => SafeAt(v, b)'
	<1> SUFFICES ASSUME Inv, Next, TypeOK',
	NEW v \in Values, NEW b \in Ballots, SafeAt(v, b)
	PROVE SafeAt(v, b)'
	OBVIOUS
	<1> USE DEF Send, Inv, Ballots
	<1> USE TRUE /\ TRUE
	<1>1. ASSUME NEW bb \in Ballots, Phase1a(bb)
	PROVE SafeAt(v, b)'
	BY <1>1, SMT DEF SafeAt, Phase1a, VotedForIn, WontVoteIn
	<1>2. ASSUME NEW a \in Acceptors, Phase1b(a)
	PROVE SafeAt(v, b)'
	BY <1>2, QuorumAssumption, SMTT(60) DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase1b
	<1>3. ASSUME NEW bb \in Ballots, Phase2a(bb)
	PROVE SafeAt(v, b)'
	BY <1>3, QuorumAssumption, SMT DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase2a
	<1>4. ASSUME NEW a \in Acceptors, Phase2b(a)
	PROVE SafeAt(v, b)'
	<2>1. PICK m \in msgs : Phase2b(a)!(m)
	BY <1>4 DEF Phase2b
	<2>2 \A aa \in Acceptors, bb \in Ballots, vv \in Values :
	VotedForIn(aa, vv, bb) => VotedForIn(aa, vv, bb)'
	BY <2>1 DEF TypeOK, VotedForIn
	<2>3. \A aa \in Acceptors, bb \in Ballots : maxBal[aa] > bb => maxBal'[aa] > bb
	BY <2>1 DEF TypeOK
	<2>4. ASSUME NEW aa \in Acceptors, NEW bb \in Ballots,
	WontVoteIn(aa, bb), NEW vv \in Values,
	VotedForIn(aa, vv, bb)'
	PROVE FALSE
	<3> DEFINE mm == [type \|-> "2b", val \|-> vv, bal \|-> bb, acc \|-> aa]
	<3>1. mm \notin msgs
	BY <2>4 DEF WontVoteIn, VotedForIn
	<3>2. mm \in msgs'
	<4>1. PICK m1 \in msgs' :
	/\ m1.type = "2b"
	/\ m1.val = vv
	/\ m1.bal = bb
	/\ m1.acc = aa
	BY <2>4 DEF VotedForIn
	<4>. QED BY <4>1 DEF TypeOK, Messages \* proved by Zenon
	<3>3. aa = a /\ m.bal = bb
	BY <2>1, <3>1, <3>2 DEF TypeOK
	<3>. QED
	BY <2>1, <2>4, <3>3 DEF Phase2b, WontVoteIn, TypeOK
	<2>5 \A aa \in Acceptors, bb \in Ballots : WontVoteIn(aa, bb) => WontVoteIn(aa, bb)'
	BY <2>3, <2>4 DEF WontVoteIn
	<2> QED
	BY <2>2, <2>5, QuorumAssumption DEF SafeAt

My question is: Has the ASSUME construct been used in the proof of SafeAtStable because Next is a disjunction of two existential quantifiers? Or could this have been written using the CASE keyword somehow?

Thank you