11.20

I am considering a simplified version and get a seemingly unprovable formula. I found a note by Lamport, A Completeness Theorem for TLA, which seems to state that TLA is complete for this formula, but I am not sure if I understand it correctly, and I have no idea about how to prove the formula within TLA framework. Can you have a look at the completeness theorem and check if this formula meets the requirements?

The simplified formula

State variables:
  For each process i \in {1, 2}:
  the flag  f_i : {0, 1}
  the log   p_i : N -> {None, 0, 1}
  the index r_i : N

# Initially, the flag is down, the log is empty, and the index is 0
Init := forall i \in {1, 2}:
  /\ f_i = 0
  /\ forall j \in N: p_i[j] = None
  /\ r_i = 0

# Actions (unmentioned variables are unchanged)
SetFlag_i := f_i' = 1

# Write current flag to the log and increment the index
WriteLog_i :=
  /\ p_i'[r_i] = f_i
  /\ r_i' = r_i + 1

Next :=
  \/ SetFlag_1 \/ SetFlag_2
  \/ WriteLog_1 \/ WriteLog_2
  \/ "stuttering"

# The Spec
LiveSpec := Init /\ []Next /\ WF(Next)

# The property: eventually, there is an index r such that both logs are 1
Property := <> (exists r \in N: p_1[r] = 1 /\ p_2[r] = 1)

# The formula
Formula := LiveSpec => Property

The Proof

LogOne_i :=  # starting from index r0, the log is either 1 or None
  <> exists r0 \in N:
     forall d  \in N:
       p_1[r0 + d] = 1 \/ p_1[r0 + d] = None

# We can prove LiveSpec => LogOne_1 and LiveSpec => LogOne_2

BothLogOne :=
  <> exists r0 \in N:
     forall d  \in N:
       (p_1[r0 + d] = 1 \/ p_1[r0 + d] = None)
    /\ (p_2[r0 + d] = 1 \/ p_2[r0 + d] = None)

# We can prove LogOne_1 /\ LogOne_2 => BothLogOne

# We can prove BothLogOne => Property