# Theory Ample_Correctness

```section ‹Correctness Theorem of Partial Order Reduction›

theory Ample_Correctness
imports
Ample_Abstract
Formula
begin

locale ample_correctness =
S: transition_system_complete ex en init int +
R: transition_system_complete ex ren init int +
F: formula_next_free φ +
ample_abstract ex en init int ind src ren
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and ind :: "'action ⇒ 'action ⇒ bool"
and src :: "'state ⇒ 'state ⇒ bool"
and ren :: "'action ⇒ 'state ⇒ bool"
and φ :: "'interpretation pltl"
begin

lemma reduction_language_indistinguishable:
assumes "R.language ⊆ F.language"
shows "S.language ⊆ F.language"
proof
fix u
assume 1: "u ∈ S.language"
obtain v where 2: "v ∈ R.language" "snth u ≈ snth v" using reduction_language_stuttering 1 by this
have 3: "v ∈ F.language" using assms 2(1) by rule
show "u ∈ F.language" using 2(2) 3 by auto
qed

theorem reduction_correct: "S.language ⊆ F.language ⟷ R.language ⊆ F.language"
using reduction_language_subset reduction_language_indistinguishable by blast

end

end```