
<1>1:





<2>1: Assume:
Prove:

<3>1:
<3>2:

Proof: By induction from <3>1 and the associativity of ``''.

<3>3:
<3>4Q.E.D.

Proof: By assumption <2>, since


<2>2: Assume:
Prove:

<3>1:
<3>2:

Proof: By induction from <3>1 and the associativity of ``''.

<3>3:

Proof: Hypothesis 1(b) (which implies
), since assumption <2> and the definition of
imply
.

<3>4Q.E.D.

Proof: By assumption <2>, since


<2>3: Assume: a tuple of constants Prove:

<3>1:
<3>2Q.E.D.

Proof: <3>1, by induction on .


<2>4:

Proof:

<2>5Q.E.D.

<1>2:

<2>1:

Proof: This is semantically obvious, since implies
but I don't know how to derive it from more primitive proof rules.

<2>2:
<2>3Q.E.D.

<1>3:

<2>1:

Proof: By the standard rule for adding history variables.

<2>2:

<3>1:

Proof: Immediate from the definitions.

<3>2Q.E.D.

Proof: <3>1 and the TLA invariance rule.


<2>3Q.E.D.

<1>4:

<2>1:

Proof: By the rules for history variables.

<2>2:

<3>1: Assume:
Prove:

<4>1: Case:

<5>1: Case:

<6>1:

Proof: Assumptions <5> and <4> and hypothesis 1(b) (which implies
).

<6>2:

Proof: <6>1, assumption <4> (
), assumption <3> (which asserts
), and the definition of .

<6>3:
Proof: Assumptions <5> and <3> (which asserts ), and the definition of .
<6>4:

Proof: <6>2, <6>3, assumptions <3> (which asserts
) and <4>, and <1>1.1.

<6>5Q.E.D.

Proof: <6>4 implies
, since
. The level<3> goal then follows from <6>1 and the definition of .


<5>2: Case:

<6>1:

Proof: Assumptions <5> and <4> and hypothesis 1(b) (which implies
).

<6>2:

Proof: <6>1, assumption <3> (which asserts ), and the definition of .

<6>3Q.E.D.

Proof: <6>1, <6>2, and the definition of imply tle level<3> goal.


<5>3Q.E.D.

<4>2: Case:

<5>1:

Proof: Assumption <3> (which asserts ), assumption <4>, which by definition of
implies
, and the definition of . 
<5>2: Case:

<6>1:
<6>2Q.E.D.

Proof: Assumptions <5> and <3> (which asserts ) imply
. The level<3> goal then follows from assumption <4> (which, by definition of
, implies
), step <6>1, and the definition of . 

<5>3: Case:

<6>1:

Proof: Assumptions <5> and <3> (which asserts ) and the definition of . 
<6>2:

Proof: By assumption <4>, since <6>1 and <5>1 imply . 
<6>3:

Proof: By assumption <5> and <6>2, since
implies
and
. 
<6>4Q.E.D.

Proof: <6>3, assumption <4> (which implies
), and the definition of imply the level<3> goal. 

<5>4Q.E.D.

<4>3: Case:

<5>1:

Proof: Assumption <3> (which asserts ), assumption <4>, and the definition of . 
<5>2Q.E.D.

Proof: <5>1, assumption <4>, and the definition of imply our level<3> goal. 

<4>4Q.E.D.

<5>1:

Proof:

<5>2Q.E.D.

Proof: By <5>1 and assumption <3> (which asserts ), cases <4>1, <4>2, and <4>3 are exhaustive. 


<3>2:

Proof: Immediate, since and are the only free variables of . 
<3>3Q.E.D.

Proof: By <3>1, <3>2, the definition of , and the usual TLA invariance rule. 

<2>3Q.E.D.

Proof: <2>1 and <2>2 and predicate logic. 

<1>5:

<2>1:

Proof: By the following rule for adding ``infinite prophecy'' variables:
If does not occur free in the temporal formula , then
.

<2>2:

<3>1:

<4>1:

Proof: By definition of and . 
<4>2:

Proof: By definition of
, since
equals
(by definition of
), which implies
. 
<4>3Q.E.D.

Proof: <4>1, <4>2, and the definition of 

<3>2:

<4>1:

<5>1:

Proof:
. 
<5>2:

Proof: <5>1 and the definition of imply
. 
<5>3Q.E.D.

Proof: <5>2 and temporal reasoning. 

<4>2:

<5>1:

Proof: Definition of 
<5>2:
<5>3Q.E.D.

Proof: <5>2 and simple temporal reasoning. 

<4>3:

Proof: By definition of
and . 
<4>4Q.E.D.

Proof: By <4>1, <4>2, <4>3, <1>2 (which implies
), and simple temporal reasoning. 

<3>3:

<4>1: Assume:
Prove:

<5>1:

Proof: Assumption <4>, since
implies
. 
<5>2: Case:

<6>1:

Proof: <5>1, assumption <5>, and the definitions of and . 
<6>2Q.E.D.

Proof: Immediate from <6>1. 

<5>3: Case:

<6>1: Case:

<7>1:

Proof: Assumptions <6> and <5> and hypothesis 1(b) (which implies
). 
<7>2:

Proof: <7>1 and assumption <4> (which asserts ) imply
. The result follows from
, assumptions <6> and <4> (which implies
), and <1>1.2. 
<7>3Q.E.D.

Let:
<8>1:

Proof: <5>1, assumption <5>, assumption <6>, assumption <4> (which implies
), and the definition of . 
<8>2:
<8>3:

Proof: <7>2 and the definition of . 
<8>4:

Proof: <8>3, assumption <5>, <5>1, and the definition of . 
<8>5Q.E.D.

Proof: <8>2 and <8>4 imply the level<4> goal. 


<6>2: Case:

<7>1: Case:

<8>1:

Proof:

<8>2:

Proof: Assumption <4> implies , which by assumption <7> implies
. By <8>1,
and assumption <6> imply
. 
<8>3:

Proof: <5>1 and assumption <5> imply
, so <8>2 implies . 
<8>4:

Proof: <5>1, assumptions <5> and <6> imply
, so
. 
<8>5Q.E.D.

Proof: <8>3 and <8>4 imply the level<4> goal. 

<7>2: Case:

<8>1:

Proof: Assumption <4> (which implies ), assumption <7>, and the definition of . 
<8>2:

Proof: Assumption <6> implies
, which with assumption <7> implies
, which equals
. 
<8>3:

Proof: <5>1 and assumption <5> imply
, so <8>2 implies . 
<8>4:

Proof: <5>1, assumption <5>, and assumption <6> imply
. By <8>1, this implies
, so
. 
<8>5Q.E.D.

Proof: <8>3 and <8>4 imply the level<4> goal. 

<7>3Q.E.D.

<6>3Q.E.D.

Proof:
Therefore, cases <6>1 and <6>2 are exhaustive. 

<5>4Q.E.D.

<4>2:

Proof: <4>1, since implies . 
<4>3:

Proof: <4>2 and simple TLA reasoning. 
<4>4Q.E.D.

<3>4Q.E.D.

<2>3Q.E.D.

<3>1:

Proof: By <2>2 and temporal predicate logic, since does not occur free in .

<3>2:

Proof: By <3>1 and temporal predicate logic.

<3>3:

Proof: By <2>2 and temporal predicate logic, since does not occur free in
.

<3>4Q.E.D.


<1>6: Assume:
Prove:

<2>1:

Proof: Assumption <1> implies , and the conclusion follows from and the definition of
. 
<2>2:

Proof: Assumption <1> implies , and the conclusion follows from and the definition of
. 
<2>3:

<3>1:

<4>1: Case:

Proof: Assumption <1> implies
, from which we deduce
, which implies the level<3> goal because
implies
. 
<4>2: Case:

<5>1:

Proof: Since
equals
, this follows from assumption <4> and hypothesis 1(c). 
<5>2:

Proof: Assumption <1> implies
. Since
implies
, assumption <4> implies
. From (11), we then deduce
, which implies the desired result since
implies
. 
<5>3Q.E.D.

Proof: The result follows immediately from <5>1 and <5>2. 

<4>3Q.E.D.

Proof: <2>1 implies that cases <4>1 and <4>2 are exhaustive. 

<3>2Q.E.D.

<4>1: Case:

Proof: By <3>1 and assumption <1>, which implies
, we have
, which implies
, and the level<2> goal follows from the definition of
. 
<4>2: Case:
<4>3Q.E.D.

Proof: <2>2 implies that cases <4>1 and <4>2 are exhaustive. 


<2>4:

<3>1: Case:

Proof: Immediate from the definition of
. 
<3>2: Case:

Proof: Assumption <1> implies
and . From
,
, and the definition of
we deduce
. From
we deduce . 
<3>3Q.E.D.

<2>5:

<3>1: Case:

Proof: Assumption <1> implies
, which by hypothesis 1(c) implies
. From
,
, and definition of
, we deduce
. 
<3>2: Case:

Proof: Assumption <1> implies
' and . From
and
we deduce
, and from
we deduce . 

<2>6Q.E.D.

<1>7:

<2>1:

Proof: Assumption <1> implies
. By hypothesis 1(a), implies
, which by
implies
, which by definition of
implies
, so
. 
<2>2: Assume:
Prove:

<3>1:

Proof: Assumption <2> implies , which implies
, which implies
. 
<3>2: Case:

<4>1: Case:

<5>1:

Proof: Assumptions <3> and <4> and hypothesis 1(b) (which implies
and
). 
<5>2:

Proof: <5>1, assumption <4>, and the definition of
. 
<5>3Q.E.D.

Proof: <5>2 and case assumption <3> imply
, which in turn implies
. 

<4>2: Case:

<5>1:

Proof: Assumption <2> implies
. Assumption <4> and implies
. The result follows from assumption <3>,
,
, and <1>1.1. 
<5>2:

Proof: Assumptions <3> and <4> and hypothesis 1(b). 
<5>3:

Proof: Assumption <2> (which implies and
), <5>2, assumption <3>, and the definition of . 
<5>4:
<5>5:

Proof: <5>2, assumption <4>, and the definition of
. 
<5>6Q.E.D.

Proof: <5>4 and <5>5 imply
, which implies
(since
implies ), which in turn implies
. 

<4>3: Case:

<5>1:

Proof: Assumptions <3> and <4> and hypothesis 1(b). 
<5>2:

Proof: <5>1, assumption <2> (which implies ), and the definition of . 
<5>3:

Proof: Assumption <2> (which implies
), <5>2, assumption <3>, and <1>1.2. 
<5>4:

Proof: <3>1, assumption <4>, assumption <3>, assumption <2> (which implies
and ), and the definition of . 
<5>5:
<5>6:

Proof: Assumption <4>, <5>1, and hypothesis 1(d). 
<5>7:

Proof: Assumption <4>, <5>1, <5>6, and the definition of
. 
<5>8Q.E.D.

Proof: <5>5 and <5>7 imply
, which implies
(since
implies ), which in turn implies
. 

<4>4Q.E.D.

<3>3: Case:

<4>1:

Proof: Assumption <2> implies , which by assumption <3> (which implies
) implies . 
<4>2:

Proof: Assumption <3> (which implies
) and the definition of
. 
<4>3:

Proof: Assumption <3> (which implies
) and hypothesis 1(c). 
<4>4:

<5>1: Case:

Proof: The definition of
implies
. 
<5>2: Case:

Proof: By <4>3, the definition of
implies
. Assumption <2> implies , which implies . 
<5>3Q.E.D.

<4>5Q.E.D.

Proof: <4>1, <4>2, and <4>4 imply
, which implies the level<2> goal. 

<3>4: Case:

<4>1:

Proof: Assumption <3> (which implies
) and hypothesis 1(d). 
<4>2:

Proof: Assumption <2> implies , which by <3>1 and assumption <3> (which implies
) implies . 
<4>3:

Proof: <4>1, assumption <3> (which implies
), and the definition of
. 
<4>4:

<5>1:

Proof: Assumption <3> (which implies
) and hypothesis 1(c). 
<5>2: Case:

Proof: <5>1 and the definition of
imply
. 
<5>3: Case:

Proof: <5>1 and the definition of
imply
. Assumption <2> implies , which implies , proving
. 
<5>4Q.E.D.

<4>5Q.E.D.

Proof: <4>2, <4>3, and <4>4 imply
, which implies the level<2> goal. 

<3>5: Case:

Proof: Assumption <2> and <1>6 imply
, which implies the level<2> goal. 
<3>6Q.E.D.

Proof: Assumption <2> implies , which equals
, so <1>1.4 implies that cases <3>2, <3>3, <3>4, and <3>5 are exhuastive. 

<2>3:

Proof: <2>2, since the definition of
implies
. 
<2>4Q.E.D.

Proof: <2>1, <2>3, and the usual TLA stepsimulation rule. 

<1>8:

<2>1:

<3>1:

Proof:
and
implies
by definition of
. 
<3>2:

Proof:
and, by hypothesis 1(d),
implies
, so
implies
by definition of
. 
<3>3:

Proof: By definition of
. 
<3>4Q.E.D.

Proof: Immediate from <3>1, <3>2, <3>3, and the definition of . 

<2>2Q.E.D.

Proof: By simple temporal reasoning from <2>1. 

<1>9:

Let:
<2>1:

<3>1: Assume:
Prove:

<4>1:

Proof: Assumption <3> and hypothesis 1(e). 
<4>2:

Proof: Assumption <3>, since implies
which implies
. 
<4>3:

<5>1:

Proof: <4>1, assumption <3> (which implies ), and the definition of . 
<5>2Q.E.D.

Proof: <5>1, assumption <3> (which implies
), and the definition of
. 

<4>4: Case:

<5>1:

Proof: <4>3, assumption <4> and hypothesis 1(b) (since
). 
<5>2:

Proof: <4>1 (which implies
), <5>1, <4>3 (which with assumption <3> implies
), assumption <3> (which implies ), and the definition of . 
<5>3:

Proof: Assumption <3> (which implies
), <4>3 (which implies ), assumption <4> (which with implies
), and <1>1.1. 
<5>4:
<5>5:

By assumption <3> (
) and the definition of
, <5>4 implies
. 
<5>6:

Proof: Assumption <4>, <5>1, and the definition of
. 
<5>7Q.E.D.

Proof: The level<3> goal follows immediately from <5>5 and <5>6. 

<4>5: Case:

<5>1:

Proof: Assumption <4>, <4>3 (which implies ), and hypothesis 1(b). 
<5>2:

Proof: Assumption <3> implies . The result then follows from <4>2, <4>5, <4>1 (which implies
), <4>3 (which by assumption <3> implies
), and the definition of . 
<5>3:

Proof: Assumption <3> implies
. By <5>1, implies
. The result then follows from <4>3 and <1>1.2. 
<5>4:
<5>5:

Proof: <5>4, assumption <3> (which asserts
), and the definition of
imply
. 
<5>6:

Proof: Case assumption <4>, <5>1, hypothesis 1(d), and the definition of
. 
<5>7Q.E.D.

Proof: The level<3> goal follows immediately from <5>5 and <5>6. 

<4>6: Case:

<5>1:

Proof: Assumption <4>, <4>3 (which implies ), and hypothesis 1(b). 
<5>2:

Proof: Case assumption <4>, <5>1, and the definition of
. 
<5>3Q.E.D.

Proof: Assumption <3>, which implies
, and <5>2 imply the level<3> goal. 

<4>7Q.E.D.

<3>2: Assume:
Prove:
<3>3: Assume:
Prove:
<3>4Q.E.D.

<2>2:
<2>3Q.E.D.

<1>10Q.E.D.

<2>1:

<3>1:

<4>1:

Proof: By definition of .

<4>2:
<4>3:

Proof: Immedate from the definition of .

<4>4:

<5>1: Case:

<6>1:

Proof: Assumption <5> and definition of .

<6>2:

Proof: Assumption <5> and definition of .

<6>3:

Proof: By definition of .

<6>4:
<6>5Q.E.D.

<5>2: Case:

<6>1:

Proof: Assumption <5> and the definition of .

<6>2: Case:
<6>3: Case:

Proof: In this case, assumption <5> implies
.

<6>4Q.E.D.

Proof: Cases <6>2 and <6>3 are exhaustive.


<5>3Q.E.D.

<4>5Q.E.D.

<3>2:

Proof: By the definition of , <3>1, repeated application of the rule
and the usual TLA rules

<3>3Q.E.D.

Proof: Follows easily from <3>2, <1>2, the definitions, and the rule that
distributes over .


<2>2:
<2>3:

Proof: <2>2 and (temporal) predicate logic.

<2>4:
<2>5:
<2>6Q.E.D.

