module CESH.Bisimulation (Node : Set) where

open import GeneralLemmas
open import CES                Node
open import CES.Properties     Node
open import CESH               Node
open import CESH.Presimulation Node
open import CESH.Properties    Node
open import CESH.Simulation    Node
open import Heap
open import MachineCode        Node
open import Relation

open Bisimulation _⟶CES_ _⟶CESH_ hiding (Bisimulation)

bisimulation : Bisimulation _⟶CES_ _⟶CESH_ R-config
bisimulation = simulation-to-bisimulation R-config simulation presimulation det
  where
    det :  a b  R-config a b  _⟶CESH_ is-deterministic-at b
    det a b x = determinism-CESH

termination-agrees :  cfg₁ cfg₂ n 
  R-config cfg₁ cfg₂  cfg₁ ↓CES nat n  cfg₂ ↓CESH nat n
termination-agrees cfg₁ cfg₂ n Rcfg₁cfg₂ =  cfg₁ cfg₂ Rcfg₁cfg₂ ,  cfg₁ cfg₂ Rcfg₁cfg₂
  where
    sim   = proj₁ bisimulation
    sim⁻¹ = proj₂ bisimulation
     :  cfg₁ cfg₂ {n}  R-config cfg₁ cfg₂  cfg₁ ↓CES nat n  cfg₂ ↓CESH nat n
     (.END , [] , val (nat n)  []) (.END , [] , [] , h) (refl , tt , ()) []
     (.END , [] , val (nat n)  []) (.END , [] , cont x  [] , h) (refl , tt , () , tt) []
     (.END , [] , val (nat n)  []) (.END , [] , x  y  s , h) (refl , tt , _ , ()) []
     (.END , [] , val (nat n)  []) (.END , x  e , s , h) (refl , () , Rs) []
     (.END , [] , val (nat n)  []) (.END , [] , val (clos _)  [] , h) (refl , tt , () , tt) []
     (.END , [] , val (nat n)  []) (.END , [] , val (nat .n)  [] , h) (refl , tt , refl , tt) [] = h , []
     cfg₁ cfg₂ Rcfg₁cfg₂ (step₁  steps) =
      let
        (cfg₂' , step₁' , Rcfg₁'cfg₂') = sim cfg₁ _ cfg₂ step₁ Rcfg₁cfg₂
        (h , steps')                   =  _ cfg₂' Rcfg₁'cfg₂' steps
       in h , step₁'  steps'
     :  cfg₁ cfg₂ {n}  R-config cfg₁ cfg₂  cfg₂ ↓CESH nat n  cfg₁ ↓CES nat n
     (.END , _  _ , s) (.END , [] , val (nat n)  [] , .h) (refl , () , Rs) (h , [])
     (.END , [] , []) (.END , [] , val (nat n)  [] , .h) (refl , tt , ()) (h , [])
     (.END , [] , x  y  s) (.END , [] , val (nat n)  [] , .h) (refl , tt , _ , ()) (h , [])
     (.END , [] , cont _  []) (.END , [] , val (nat n)  [] , .h) (refl , tt , () , tt) (h , [])
     (.END , [] , val (clos _)  []) (.END , [] , val (nat n)  [] , .h) (refl , tt , () , tt) (h , [])
     (.END , [] , val (nat .n)  []) (.END , [] , val (nat n)  [] , .h) (refl , tt , refl , tt) (h , []) = []
     cfg₁ cfg₂ Rcfg₁cfg₂ (h , step₁'  steps') =
       let
         (cfg₁' , step₁ , Rcfg₁'cfg₂') = sim⁻¹ cfg₂ _ cfg₁ step₁' Rcfg₁cfg₂
         steps                         =  cfg₁' _ Rcfg₁'cfg₂' (h , steps')
        in step₁  steps

divergence-agrees :  cfg₁ cfg₂ 
  R-config cfg₁ cfg₂  cfg₁ ↑CES  cfg₂ ↑CESH
divergence-agrees cfg₁ cfg₂ Rcfg₁cfg₂ = divergence-bisimulation cfg₁ cfg₂ (_ , bisimulation , Rcfg₁cfg₂)

initial-related :  c  R-config (c , [] , []) (c , [] , [] , )
initial-related c = refl , tt , tt

initial-termination-agrees :  c n  (c , [] , []) ↓CES nat n  (c , [] , [] , ) ↓CESH nat n
initial-termination-agrees c n = termination-agrees (c , [] , []) (c , [] , [] , ) n (initial-related c)

initial-divergence-agrees :  c  (c , [] , []) ↑CES  (c , [] , [] , ) ↑CESH
initial-divergence-agrees c = divergence-agrees (c , [] , []) (c , [] , [] , ) (initial-related c)