Theory "bisimulation"

Parents relation

Signature

Constant	Type
BISIM	:(α -> β -> α -> bool) -> (α -> α -> bool) -> bool
BISIM_REL	:(α -> β -> α -> bool) -> α -> α -> bool
ETS	:(α -> β -> α -> bool) -> β -> α -> α -> bool
WBISIM	:(α -> β -> α -> bool) -> β -> (α -> α -> bool) -> bool
WBISIM_REL	:(α -> β -> α -> bool) -> β -> α -> α -> bool
WTS	:(α -> β -> α -> bool) -> β -> α -> β -> α -> bool

Definitions

WTS_def

⊢ ∀ts tau.
      WTS ts tau =
      (λp l q. ∃p' q'. ETS ts tau p p' ∧ ts p' l q' ∧ ETS ts tau q' q)

WBISIM_def

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

ETS_def

⊢ ∀ts tau. ETS ts tau = (λx y. ts x tau y)⃰

BISIM_def

⊢ ∀ts R.
      BISIM ts R ⇔
      ∀p q l.
          R p q ⇒
          (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q') ∧
          ∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ R p' q'

Theorems

WBISIM_RUNION

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

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_REL_IS_WBISIM

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

WBISIM_REL_IS_EQUIV_REL

⊢ ∀ts tau. equivalence (WBISIM_REL ts tau)

WBISIM_REL_def

⊢ ∀ts tau. WBISIM_REL ts tau = (λp q. ∃R. WBISIM ts tau R ∧ R 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_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_O

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

WBISIM_INV

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

WBISIM_ID

⊢ ∀ts tau. WBISIM ts tau $=

TS_IMP_WTS

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

TS_IMP_ETS

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

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'

ETS_TRANS

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

ETS_REFL

⊢ ∀ts tau p. ETS ts tau p p

BISIM_RUNION

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

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_RSUBSET_WBISIM_REL

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

BISIM_REL_IS_EQUIV_REL

⊢ ∀ts. equivalence (BISIM_REL ts)

BISIM_REL_IS_BISIM

⊢ ∀ts. BISIM ts (BISIM_REL ts)

BISIM_REL_IMP_WBISIM_REL

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

BISIM_REL_def

⊢ ∀ts. BISIM_REL ts = (λp q. ∃R. BISIM ts R ∧ R 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_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_O

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

BISIM_INV

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

BISIM_IMP_WBISIM

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

BISIM_ID

⊢ ∀ts. BISIM ts $=