- stateSpaceProduct_comm_thm
-
|- ∀ss1 ss2 vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2 ⇒
(stateSpaceProduct ss1 ss2 = stateSpaceProduct ss2 ss1)
- stateSpaceProduct_assoc_thm
-
|- ∀ss1 ss2 ss3.
stateSpaceProduct ss1 (stateSpaceProduct ss2 ss3) =
stateSpaceProduct (stateSpaceProduct ss1 ss2) ss3
- stateSpaceProduct_left_comm_thm
-
|- ∀ss1 ss2 ss3 vs1 vs2 vs3.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ stateSpace ss3 vs3 ∧
DISJOINT vs1 vs2 ∧ DISJOINT vs1 vs3 ⇒
(stateSpaceProduct ss1 (stateSpaceProduct ss2 ss3) =
stateSpaceProduct ss2 (stateSpaceProduct ss1 ss3))
- invariantStateSpace_thm_7
-
|- ∀ss dom vs1 vs2.
stateSpace ss dom ∧ dom ⊆ vs1 ∪ vs2 ⇒
ss ⊆ stateSpaceProduct (ss_proj ss vs1) (ss_proj ss vs2)
- invariantStateSpace_thm_8
-
|- ∀ss1 ss2 ss3 ss4.
ss1 ⊆ ss3 ∧ ss2 ⊆ ss4 ⇒
stateSpaceProduct ss1 ss2 ⊆ stateSpaceProduct ss3 ss4
- invariantStateSpace_thm_10_1
-
|- ∀ss1 ss2 vs.
stateSpaceProduct (ss_proj ss1 vs) (ss_proj ss2 vs) =
ss_proj (stateSpaceProduct ss1 ss2) vs
- invariantStateSpace_thm_11
-
|- ∀ss1 ss2 vs.
stateSpaceProduct (ss_proj ss1 vs) (ss_proj ss2 vs) ⊆
ss_proj (stateSpaceProduct ss1 ss2) vs
- PROD_rules
-
|- (∀ss. PROD ∅ ss ss) ∧
∀ss SS ss' ss''.
ss ∉ SS ∧ PROD SS ss' ss'' ⇒
PROD (ss INSERT SS) ss' (stateSpaceProduct ss ss'')
- PROD_ind
-
|- ∀PROD'.
(∀ss. PROD' ∅ ss ss) ∧
(∀ss SS ss' ss''.
ss ∉ SS ∧ PROD' SS ss' ss'' ⇒
PROD' (ss INSERT SS) ss' (stateSpaceProduct ss ss'')) ⇒
∀a0 a1 a2. PROD a0 a1 a2 ⇒ PROD' a0 a1 a2
- PROD_strongind
-
|- ∀PROD'.
(∀ss. PROD' ∅ ss ss) ∧
(∀ss SS ss' ss''.
ss ∉ SS ∧ PROD SS ss' ss'' ∧ PROD' SS ss' ss'' ⇒
PROD' (ss INSERT SS) ss' (stateSpaceProduct ss ss'')) ⇒
∀a0 a1 a2. PROD a0 a1 a2 ⇒ PROD' a0 a1 a2
- PROD_cases
-
|- ∀a0 a1 a2.
PROD a0 a1 a2 ⇔
(a0 = ∅) ∧ (a2 = a1) ∨
∃ss SS ss''.
(a0 = ss INSERT SS) ∧ (a2 = stateSpaceProduct ss ss'') ∧ ss ∉ SS ∧
PROD SS a1 ss''
- PROD_empty
-
|- PROD ∅ a b ⇔ (a = b)
- FINITE_PROD_result
-
|- ∀s. FINITE s ⇒ ∀a. ∃b. PROD s a b
- PROD_FINITE
-
|- ∀s a b. PROD s a b ⇒ FINITE s
- IN_INSERT_EXISTS
-
|- x ∈ s ⇔ ∃s0. (s = x INSERT s0) ∧ x ∉ s0
- PROD_det
-
|- ∀s a b.
PROD s a b ⇒
(∀ss1 ss2.
ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
∃vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
(∀ss. ss ∈ s ⇒ ∃vs. stateSpace ss vs) ⇒
∀c. PROD s a c ⇒ (b = c)
- PRODf_EMPTY
-
|- PRODf ∅ a = a
- PRODf_INSERT
-
|- ∀e s.
FINITE s ∧ e ∉ s ∧ e ≠ ∅ ∧
(∀ss1 ss2.
ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
∃vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
(∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧ (∃vse. stateSpace e vse) ∧
(∀ss.
ss ∈ s ⇒
∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ⇒
∀a. PRODf (e INSERT s) a = stateSpaceProduct e (PRODf s a)
- FINITE_stateSpaceProduct
-
|- ∀ss1 ss2. FINITE ss1 ∧ FINITE ss2 ⇒ FINITE (stateSpaceProduct ss1 ss2)
- PRODf_FINITE
-
|- ∀s.
FINITE s ⇒
∀e.
e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧ (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
(∀ss1 ss2.
ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
∃vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
(∀ss.
ss ∈ s ⇒
∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
FINITE (PRODf s e)
- PRODf_FINITE'
-
|- ∀s e.
FINITE s ∧ e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧
(∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
(∀ss1 ss2.
ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
∃vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
(∀ss.
ss ∈ s ⇒
∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
FINITE (PRODf s e)
- stateSpaceProduct_CARD
-
|- ∀ss1 ss2.
FINITE ss1 ∧ FINITE ss2 ⇒
CARD (stateSpaceProduct ss1 ss2) ≤ CARD ss1 * CARD ss2
- PRODf_CARD
-
|- ∀s.
FINITE s ⇒
∀e.
e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧ (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
(∀ss1 ss2.
ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
∃vs1 vs2.
stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
(∀ss.
ss ∈ s ⇒
∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
CARD (PRODf s e) ≤ Π CARD (e INSERT s)