<> (\A entry \in {[term |-> Nat, index |-> Nat, value |-> Nat]} : entry \in AllServerQuorumLogs ~> entry \in RANGE(committedLogs))
<> (\A entry \in [term: 1..MaxTerm, index: 1..MaxIndex, value: 1..MaxValue] : entry \in AllServerQuorumLogs ~> entry \in RANGE(committedLogs))
MaxTerm, MaxIndex and MaxValue are constants .