|
<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 step-simulation 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.
|
|