HomeIsabelle/Phabricator
Diffusion afp-devel db7040379c22

Proof of Restricted Master Theorem on LTL
db7040379c22
Actions

Description

Proof of Restricted Master Theorem on LTL

Details

Provenance
Benedikt Seidl <benedikt.seidl@tum.de>Authored on
Parents
rAFPef5c588d2a90: Patched some failing proofs
Branches
Unknown
Tags
Unknown

Event Timeline

Changes (11)

PathSize
LTL/

rAFPdb7040379c22

View Options

thys/LTL/Equivalence_Relations.thy

Loading...
View Options

thys/LTL/LTL.thy

Loading...
View Options

thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy

Loading...
View Options

thys/LTL_Master_Theorem/Logical_Characterization/After.thy

Loading...
View Options

thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy

Loading...
View Options

thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy

Loading...
View Options

thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy

Loading...
View Options

thys/LTL_Master_Theorem/ROOT

Loading...