class DY.ReachableImpliesInvariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (config : ReachabilityConfig) : Prop

• pf (input : config.Input) : HoareTriple (config.step input).snd (fun (tr : ProofTrace) => config.PreCond input (Trace.erase tr)) fun (x : (config.step input).fst) (x_1 : ProofTrace) => True

instance DY.instReachableImpliesInvariantCombine [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α : Type} (configs : α → ReachabilityConfig) [insts : ∀ (id : α), ReachableImpliesInvariant (configs id)] : ReachableImpliesInvariant (ReachabilityConfig.combine configs)

theorem DY.Trace.Reachable_implies_Invariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (config : ReachabilityConfig) [inst : ReachableImpliesInvariant config] (trExec : ExecTrace) : Reachable config trExec → ∃ (trProof : ProofTrace), erase trProof = trExec ∧ Invariant trProof

theorem DY.Trace.apply_Reachable_implies_Invariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {config : ReachabilityConfig} [inst : ReachableImpliesInvariant config] {p : ExecTrace → Prop} : (∀ (trProof : ProofTrace), Invariant trProof → p (erase trProof)) → ∀ (trExec : ExecTrace), Reachable config trExec → p trExec