[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Proof step 49 from proof map-path (
previous step
)
path(x, r0, r1, H), closed(H), inj(map), reachset(r0, H) ⊆ dom map ⊦ path(x, map[r0], map[r1], apply(H, map)) ∧ r0 ∈ map ∧ r1 ∈ map
Heuristic simplifier applied rule simplifier
And closed the goal!
Rule argument
Additional information
[Concretesimprules((Csimpnamedseq(path-first-in,,, ⊦ path(x, r0, r1, H) → r0 ∈ H)))]