{"size": 1161, "ext": "scrbl", "max_stars_repo_path": "dissertation/proofs.scrbl", "max_stars_repo_name": "florence/esterel-calculus", "max_stars_repo_stars_event_min_datetime": "2020-04-16T10:58:53.000Z", "max_stars_repo_stars_event_max_datetime": "2020-07-01T03:59:31.000Z", "max_issues_repo_path": "dissertation/proofs.scrbl", "max_issues_repo_name": "florence/esterel-calculus", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "dissertation/proofs.scrbl", "max_forks_repo_name": "florence/esterel-calculus", "max_forks_repo_forks_event_min_datetime": "2020-04-15T20:02:49.000Z", "max_forks_repo_forks_event_max_datetime": "2020-04-15T20:02:49.000Z"}
{"max_stars_count": 3, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 32.25, "max_line_length": 63, "alphanum_fraction": 0.6701119724}
#lang scribble/book

@(require "lib/redex-rewrite.rkt"
          "lib/util.rkt"
          "lib/proofs.rkt"
          "lib/proof-extras.rkt"
          "lib/misc-figures.rkt"
          "lib/rule-figures.rkt"
          "lib/jf-figures.rkt"
          "lib/cite.rkt"
          (only-in "notations.scrbl")
          (only-in "proofs/proofs.scrbl")
          esterel-calculus/redex/model/shared
          scriblib/figure
          redex/pict
          syntax/parse/define
          esterel-calculus/redex/model/deps
          (for-syntax racket/base)
          pict)


@title[#:style paper-title-style
       #:tag "sec:proofs"]{Proving the calculus correct}


The three properties for the calculus which require proof
are consistency, soundness, and adequacy. This section provides
an overview of those proofs. This section
relies heavily on the background given in
@secref["background-circuits"], as well as the descriptions
of the properties given in @secref["intro"].

@include-section["justification/setup.scrbl"]
@include-section["justification/soundness.scrbl"]
@include-section["justification/adequacy.scrbl"]
@include-section["justification/consistent.scrbl"]