Skip to content
This repository has been archived by the owner on Feb 5, 2022. It is now read-only.

Add skeletons of unidirectional_bridge core lemmas #34

Closed
jeltsch opened this issue May 15, 2019 · 0 comments · Fixed by #53
Closed

Add skeletons of unidirectional_bridge core lemmas #34

jeltsch opened this issue May 15, 2019 · 0 comments · Fixed by #53
Assignees
@jeltsch
Labels
language: isabelle topic: process calculus type: enhancement
Projects
Formally prove relaying–broadcasting ...
Milestone
2019-05-27 meeting

Comments

@jeltsch
Copy link
Contributor

jeltsch commented May 15, 2019

Our goal is to add skeletons of the following core lemmas about unidirectional_bridge:

shortcut_addition:
  a → b ∥ b → c ≈⇩♭ a → b ∥ b → c ∥ a → c
loop_redundancy_under_duploss:
  ¤⇧*a ∥ a → a ≈⇩♭ ¤⇧*a
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@jeltsch jeltsch

Labels
language: isabelle topic: process calculus type: enhancement
Projects
No open projects
Formally prove relaying–broadcasting ...
  
Done
Milestone
2019-05-27 meeting
Development

Successfully merging a pull request may close this issue.

Add skeletons of unidirectional_bridge core lemmas input-output-hk/high-assurance-legacy
1 participant
@jeltsch