set -xe
# Noduplicity must be checked in the case with m >= 2
# CInit4 == t = 1 /\ n = 4 /\ mmax = 2 /\ smax = 1
cinit=CInit4
model=MBRB_abs_12.tla

# Lemma NoduplicitySig
./check_inductive.sh $model $cinit InitNoduplicity Noduplicity

# Lemma TypeOK
./check_inductive.sh $model $cinit TypeOK TypeOK

# Lemma PacketsValid
./check_inductive.sh $model $cinit InitPacketsValid11 PacketsValid11

# Lemma NoduplicitySig
./check_inductive.sh $model $cinit InitNoduplicitySig NoduplicitySig

# Lemma Delivered111MeansSigned
./check_inductive.sh $model $cinit Delivered111MeansSigned InitDelivered111MeansSigned