Theory: bisimulation

Theorems

BISIM_ID

⊢ ∀ts. BISIM ts $=

BISIM_IMP_WBISIM

⊢ ∀ts tau R. BISIM ts R ⇒ WBISIM ts tau R

BISIM_INV

⊢ ∀ts R. BISIM ts R ⇒ BISIM ts Rᵀ

BISIM_O

⊢ ∀ts R R'. BISIM ts R ∧ BISIM ts R' ⇒ BISIM ts (R' ∘ᵣ R)

BISIM_REL_IMP_WBISIM_REL

⊢ ∀ts tau p q. BISIM_REL ts p q ⇒ WBISIM_REL ts tau p q

BISIM_REL_IS_BISIM

⊢ ∀ts. BISIM ts (BISIM_REL ts)

BISIM_REL_IS_EQUIV_REL

⊢ ∀ts. equivalence (BISIM_REL ts)

BISIM_REL_RSUBSET_WBISIM_REL

⊢ ∀ts tau. BISIM_REL ts ⊆ᵣ WBISIM_REL ts tau

BISIM_REL_cases

⊢ ∀ts a0 a1.
    BISIM_REL ts a0 a1 ⇔
    ∀l. (∀p'. ts a0 l p' ⇒ ∃q'. ts a1 l q' ∧ BISIM_REL ts p' q') ∧
        ∀q'. ts a1 l q' ⇒ ∃p'. ts a0 l p' ∧ BISIM_REL ts p' q'

BISIM_REL_coind

⊢ ∀ts BISIM_REL'.
    (∀a0 a1.
       BISIM_REL' a0 a1 ⇒
       ∀l. (∀p'. ts a0 l p' ⇒ ∃q'. ts a1 l q' ∧ BISIM_REL' p' q') ∧
           ∀q'. ts a1 l q' ⇒ ∃p'. ts a0 l p' ∧ BISIM_REL' p' q') ⇒
    ∀a0 a1. BISIM_REL' a0 a1 ⇒ BISIM_REL ts a0 a1

BISIM_REL_def

⊢ ∀ts. BISIM_REL ts = (λp q. ∃R. BISIM ts R ∧ R p q)

BISIM_REL_rules

⊢ ∀ts p q.
    (∀l. (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ BISIM_REL ts p' q') ∧
         ∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ BISIM_REL ts p' q') ⇒
    BISIM_REL ts p q

BISIM_REL_strong_thm

⊢ BISIM_REL ts p0 q0 ⇔
  ∃R. R p0 q0 ∧
      ∀p q.
        R p q ⇒
        ∀l. (∀p'.
               ts p l p' ⇒ ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q')) ∧
            ∀q'.
              ts q l q' ⇒ ∃p'. ts p l p' ∧ (R p' q' ∨ BISIM_REL ts p' q')

BISIM_REL_sym

⊢ symmetric (BISIM_REL ts)

BISIM_REL_sym_strong_thm

⊢ BISIM_REL ts p0 q0 ⇔
  ∃R. symmetric R ∧ R p0 q0 ∧
      ∀p q.
        R p q ⇒
        ∀l p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q')

BISIM_REL_sym_thm

⊢ BISIM_REL ts p0 q0 ⇔
  ∃R. symmetric R ∧ R p0 q0 ∧
      ∀p q. R p q ⇒ ∀l p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q'

BISIM_RUNION

⊢ ∀ts R R'. BISIM ts R ∧ BISIM ts R' ⇒ BISIM ts (R ∪ᵣ R')

ETS_REFL

⊢ ∀ts tau p. ETS ts tau p p

ETS_TRANS

⊢ ∀ts tau x y z. ETS ts tau x y ∧ ETS ts tau y z ⇒ ETS ts tau x z

ETS_WTS_ETS

⊢ ∀ts tau p p1 l p2 p'.
    ETS ts tau p p1 ∧ WTS ts tau p1 l p2 ∧ ETS ts tau p2 p' ⇒
    WTS ts tau p l p'

TS_IMP_ETS

⊢ ∀ts tau p q. ts p tau q ⇒ ETS ts tau p q

TS_IMP_WTS

⊢ ∀ts tau p l q. ts p l q ⇒ WTS ts tau p l q

WBISIM_ID

⊢ ∀ts tau. WBISIM ts tau $=

WBISIM_INV

⊢ ∀ts tau R. WBISIM ts tau R ⇒ WBISIM ts tau Rᵀ

WBISIM_O

⊢ ∀ts tau R R'.
    WBISIM ts tau R ∧ WBISIM ts tau R' ⇒ WBISIM ts tau (R' ∘ᵣ R)

WBISIM_REL_IS_EQUIV_REL

⊢ ∀ts tau. equivalence (WBISIM_REL ts tau)

WBISIM_REL_IS_WBISIM

⊢ ∀ts tau. WBISIM ts tau (WBISIM_REL ts tau)

WBISIM_REL_cases

⊢ ∀ts tau a0 a1.
    WBISIM_REL ts tau a0 a1 ⇔
    (∀l. l ≠ tau ⇒
         (∀p'.
            ts a0 l p' ⇒ ∃q'. WTS ts tau a1 l q' ∧ WBISIM_REL ts tau p' q') ∧
         ∀q'.
           ts a1 l q' ⇒ ∃p'. WTS ts tau a0 l p' ∧ WBISIM_REL ts tau p' q') ∧
    (∀p'. ts a0 tau p' ⇒ ∃q'. ETS ts tau a1 q' ∧ WBISIM_REL ts tau p' q') ∧
    ∀q'. ts a1 tau q' ⇒ ∃p'. ETS ts tau a0 p' ∧ WBISIM_REL ts tau p' q'

WBISIM_REL_coind

⊢ ∀ts tau WBISIM_REL'.
    (∀a0 a1.
       WBISIM_REL' a0 a1 ⇒
       (∀l. l ≠ tau ⇒
            (∀p'. ts a0 l p' ⇒ ∃q'. WTS ts tau a1 l q' ∧ WBISIM_REL' p' q') ∧
            ∀q'. ts a1 l q' ⇒ ∃p'. WTS ts tau a0 l p' ∧ WBISIM_REL' p' q') ∧
       (∀p'. ts a0 tau p' ⇒ ∃q'. ETS ts tau a1 q' ∧ WBISIM_REL' p' q') ∧
       ∀q'. ts a1 tau q' ⇒ ∃p'. ETS ts tau a0 p' ∧ WBISIM_REL' p' q') ⇒
    ∀a0 a1. WBISIM_REL' a0 a1 ⇒ WBISIM_REL ts tau a0 a1

WBISIM_REL_def

⊢ ∀ts tau. WBISIM_REL ts tau = (λp q. ∃R. WBISIM ts tau R ∧ R p q)

WBISIM_REL_rules

⊢ ∀ts tau p q.
    (∀l. l ≠ tau ⇒
         (∀p'. ts p l p' ⇒ ∃q'. WTS ts tau q l q' ∧ WBISIM_REL ts tau p' q') ∧
         ∀q'. ts q l q' ⇒ ∃p'. WTS ts tau p l p' ∧ WBISIM_REL ts tau p' q') ∧
    (∀p'. ts p tau p' ⇒ ∃q'. ETS ts tau q q' ∧ WBISIM_REL ts tau p' q') ∧
    (∀q'. ts q tau q' ⇒ ∃p'. ETS ts tau p p' ∧ WBISIM_REL ts tau p' q') ⇒
    WBISIM_REL ts tau p q

WBISIM_RUNION

⊢ ∀ts tau R R'.
    WBISIM ts tau R ∧ WBISIM ts tau R' ⇒ WBISIM ts tau (R ∪ᵣ R')

Theory bisimulation

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems