Theory ASC_Hoare
theory ASC_Hoare
imports ASC_Sufficiency "HOL-Hoare.Hoare_Logic"
begin
section ‹ Correctness of the Adaptive State Counting Algorithm in Hoare-Logic ›
text ‹
In this section we give an example implementation of the adaptive state counting algorithm in a
simple WHILE-language and prove that this implementation produces a certain output if and only if
input FSM @{verbatim M1} is a reduction of input FSM @{verbatim M2}.
›
lemma atc_io_reduction_on_sets_from_obs :
assumes "L⇩i⇩n M1 T ⊆ L⇩i⇩n M2 T"
and "(⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω) ⊆ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
shows "atc_io_reduction_on_sets M1 T Ω M2"
unfolding atc_io_reduction_on_sets.simps atc_io_reduction_on.simps
proof
fix iseq assume "iseq ∈ T"
have "L⇩i⇩n M1 {iseq} ⊆ L⇩i⇩n M2 {iseq}"
by (metis ‹iseq ∈ T› assms(1) bot.extremum insert_mono io_reduction_on_subset
mk_disjoint_insert)
moreover have "∀io∈L⇩i⇩n M1 {iseq}. B M1 io Ω ⊆ B M2 io Ω"
proof
fix io assume "io ∈ L⇩i⇩n M1 {iseq}"
then have "io ∈ L⇩i⇩n M2 {iseq}"
using calculation by blast
show "B M1 io Ω ⊆ B M2 io Ω "
proof
fix x assume "x ∈ B M1 io Ω"
have "io ∈ L⇩i⇩n M1 T"
using ‹io ∈ L⇩i⇩n M1 {iseq}› ‹iseq ∈ T› by auto
moreover have "(io,x) ∈ {io} × B M1 io Ω"
using ‹x ∈ B M1 io Ω› by blast
ultimately have "(io,x) ∈ (⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω)"
by blast
then have "(io,x) ∈ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
using assms(2) by blast
then have "(io,x) ∈ {io} × B M2 io Ω"
by blast
then show "x ∈ B M2 io Ω"
by blast
qed
qed
ultimately show "L⇩i⇩n M1 {iseq} ⊆ L⇩i⇩n M2 {iseq}
∧ (∀io∈L⇩i⇩n M1 {iseq}. B M1 io Ω ⊆ B M2 io Ω)"
by linarith
qed
lemma atc_io_reduction_on_sets_to_obs :
assumes "atc_io_reduction_on_sets M1 T Ω M2"
shows "L⇩i⇩n M1 T ⊆ L⇩i⇩n M2 T"
and "(⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω) ⊆ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
proof
fix x assume "x ∈ L⇩i⇩n M1 T"
show "x ∈ L⇩i⇩n M2 T"
using assms unfolding atc_io_reduction_on_sets.simps atc_io_reduction_on.simps
proof -
assume a1: "∀iseq∈T. L⇩i⇩n M1 {iseq} ⊆ L⇩i⇩n M2 {iseq}
∧ (∀io∈L⇩i⇩n M1 {iseq}. B M1 io Ω ⊆ B M2 io Ω)"
have f2: "x ∈ UNION T (language_state_for_input M1 (initial M1))"
by (metis (no_types) ‹x ∈ L⇩i⇩n M1 T› language_state_for_inputs_alt_def)
obtain aas :: "'a list set ⇒ ('a list ⇒ ('a × 'b) list set) ⇒ ('a × 'b) list ⇒ 'a list"
where
"∀x0 x1 x2. (∃v3. v3 ∈ x0 ∧ x2 ∈ x1 v3) = (aas x0 x1 x2 ∈ x0 ∧ x2 ∈ x1 (aas x0 x1 x2))"
by moura
then have "∀ps f A. (ps ∉ UNION A f ∨ aas A f ps ∈ A ∧ ps ∈ f (aas A f ps))
∧ (ps ∈ UNION A f ∨ (∀as. as ∉ A ∨ ps ∉ f as))"
by blast
then show ?thesis
using f2 a1 by (metis (no_types) contra_subsetD language_state_for_input_alt_def
language_state_for_inputs_alt_def)
qed
next
show "(⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω) ⊆ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
proof
fix iox assume "iox ∈ (⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω)"
then obtain io x where "iox = (io,x)"
by blast
have "io ∈ L⇩i⇩n M1 T"
using ‹iox = (io, x)› ‹iox ∈ (⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω)› by blast
have "(io,x) ∈ {io} × B M1 io Ω"
using ‹iox = (io, x)› ‹iox ∈ (⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω)› by blast
then have "x ∈ B M1 io Ω"
by blast
then have "x ∈ B M2 io Ω"
using assms unfolding atc_io_reduction_on_sets.simps atc_io_reduction_on.simps
by (metis (no_types, lifting) UN_E ‹io ∈ L⇩i⇩n M1 T› language_state_for_input_alt_def
language_state_for_inputs_alt_def subsetCE)
then have "(io,x) ∈ {io} ×B M2 io Ω"
by blast
then have "(io,x) ∈ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
using ‹io ∈ L⇩i⇩n M1 T› by auto
then show "iox ∈ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω)"
using ‹iox = (io, x)› by auto
qed
qed
lemma atc_io_reduction_on_sets_alt_def :
shows "atc_io_reduction_on_sets M1 T Ω M2 =
(L⇩i⇩n M1 T ⊆ L⇩i⇩n M2 T
∧ (⋃io∈L⇩i⇩n M1 T. {io} × B M1 io Ω)
⊆ (⋃io∈L⇩i⇩n M2 T. {io} × B M2 io Ω))"
using atc_io_reduction_on_sets_to_obs[of M1 T Ω M2]
and atc_io_reduction_on_sets_from_obs[of M1 T M2 Ω]
by blast
lemma asc_algorithm_correctness:
"VARS tsN cN rmN obs obsI obs⇩Ω obsI⇩Ω iter isReduction
{
OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω
}
tsN := {};
cN := V;
rmN := {};
obs := L⇩i⇩n M2 cN;
obsI := L⇩i⇩n M1 cN;
obs⇩Ω := (⋃io∈L⇩i⇩n M2 cN. {io} × B M2 io Ω);
obsI⇩Ω := (⋃io∈L⇩i⇩n M1 cN. {io} × B M1 io Ω);
iter := 1;
WHILE (cN ≠ {} ∧ obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω)
INV {
0 < iter
∧ tsN = TS M2 M1 Ω V m (iter-1)
∧ cN = C M2 M1 Ω V m iter
∧ rmN = RM M2 M1 Ω V m (iter-1)
∧ obs = L⇩i⇩n M2 (tsN ∪ cN)
∧ obsI = L⇩i⇩n M1 (tsN ∪ cN)
∧ obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)
∧ obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)
∧ OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω
}
DO
iter := iter + 1;
rmN := {xs' ∈ cN .
(¬ (L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}))
∨ (∀ io ∈ L⇩i⇩n M1 {xs'} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'' ))))};
tsN := tsN ∪ cN;
cN := append_set (cN - rmN) (inputs M2) - tsN;
obs := obs ∪ L⇩i⇩n M2 cN;
obsI := obsI ∪ L⇩i⇩n M1 cN;
obs⇩Ω := obs⇩Ω ∪ (⋃io∈L⇩i⇩n M2 cN. {io} × B M2 io Ω);
obsI⇩Ω := obsI⇩Ω ∪ (⋃io∈L⇩i⇩n M1 cN. {io} × B M1 io Ω)
OD;
isReduction := ((obsI ⊆ obs) ∧ (obsI⇩Ω ⊆ obs⇩Ω))
{
isReduction = M1 ≼ M2
}"
proof (vcg)
assume precond : "OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω"
have "{} = TS M2 M1 Ω V m (1-1)"
"V = C M2 M1 Ω V m 1"
"{} = RM M2 M1 Ω V m (1-1)"
"L⇩i⇩n M2 V = L⇩i⇩n M2 ({} ∪ V)"
"L⇩i⇩n M1 V = L⇩i⇩n M1 ({} ∪ V)"
"(⋃io∈L⇩i⇩n M2 V. {io} × B M2 io Ω)
= (⋃io∈L⇩i⇩n M2 ({} ∪ V). {io} × B M2 io Ω)"
"(⋃io∈L⇩i⇩n M1 V. {io} × B M1 io Ω)
= (⋃io∈L⇩i⇩n M1 ({} ∪ V). {io} × B M1 io Ω)"
using precond by auto
moreover have "OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω "
using precond by assumption
ultimately show "0 < (1::nat) ∧
{} = TS M2 M1 Ω V m (1 - 1) ∧
V = C M2 M1 Ω V m 1 ∧
{} = RM M2 M1 Ω V m (1 - 1) ∧
L⇩i⇩n M2 V = L⇩i⇩n M2 ({} ∪ V) ∧
L⇩i⇩n M1 V = L⇩i⇩n M1 ({} ∪ V) ∧
(⋃io∈L⇩i⇩n M2 V. {io} × B M2 io Ω)
= (⋃io∈L⇩i⇩n M2 ({} ∪ V). {io} × B M2 io Ω) ∧
(⋃io∈L⇩i⇩n M1 V. {io} × B M1 io Ω)
= (⋃io∈L⇩i⇩n M1 ({} ∪ V). {io} × B M1 io Ω) ∧
OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω"
by linarith+
next
fix tsN cN rmN obs obsI obs⇩Ω obsI⇩Ω iter isReduction
assume precond : "(0 < iter ∧
tsN = TS M2 M1 Ω V m (iter - 1) ∧
cN = C M2 M1 Ω V m iter ∧
rmN = RM M2 M1 Ω V m (iter - 1) ∧
obs = L⇩i⇩n M2 (tsN ∪ cN) ∧
obsI = L⇩i⇩n M1 (tsN ∪ cN) ∧
obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω) ∧
obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω) ∧
OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω)
∧ cN ≠ {} ∧ obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω"
then have "0 < iter"
"OFSM M1"
"OFSM M2"
"asc_fault_domain M2 M1 m"
"test_tools M2 M1 FAIL PM V Ω"
"cN ≠ {}"
"obsI ⊆ obs"
"tsN = TS M2 M1 Ω V m (iter-1)"
"cN = C M2 M1 Ω V m iter"
"rmN = RM M2 M1 Ω V m (iter-1)"
"obs = L⇩i⇩n M2 (tsN ∪ cN)"
"obsI = L⇩i⇩n M1 (tsN ∪ cN)"
"obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)"
"obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)"
by linarith+
obtain k where "iter = Suc k"
using gr0_implies_Suc[OF ‹0 < iter›] by blast
then have "cN = C M2 M1 Ω V m (Suc k)"
"tsN = TS M2 M1 Ω V m k"
using ‹cN = C M2 M1 Ω V m iter› ‹tsN = TS M2 M1 Ω V m (iter-1)› by auto
have "TS M2 M1 Ω V m iter = TS M2 M1 Ω V m (Suc k)"
"C M2 M1 Ω V m iter = C M2 M1 Ω V m (Suc k)"
"RM M2 M1 Ω V m iter = RM M2 M1 Ω V m (Suc k)"
using ‹iter = Suc k› by presburger+
have rmN_calc[simp] : "{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')} =
RM M2 M1 Ω V m iter"
proof -
have "{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')} =
{xs' ∈ C M2 M1 Ω V m (Suc k).
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs ((TS M2 M1 Ω V m k) ∪ V) S1 Ω V'')}"
using ‹cN = C M2 M1 Ω V m (Suc k)› ‹tsN = TS M2 M1 Ω V m k› by blast
moreover have "{xs' ∈ C M2 M1 Ω V m (Suc k).
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs ((TS M2 M1 Ω V m k) ∪ V) S1 Ω V'')} =
RM M2 M1 Ω V m (Suc k)"
using RM.simps(2)[of M2 M1 Ω V m k] by blast
ultimately have "{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')} =
RM M2 M1 Ω V m (Suc k)"
by presburger
then show ?thesis
using ‹iter = Suc k› by presburger
qed
moreover have "RM M2 M1 Ω V m iter = RM M2 M1 Ω V m (iter + 1 - 1)" by simp
ultimately have rmN_calc' : "{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')} =
RM M2 M1 Ω V m (iter + 1 - 1)" by presburger
have "tsN ∪ cN = TS M2 M1 Ω V m (Suc k)"
proof (cases k)
case 0
then show ?thesis
using ‹tsN = TS M2 M1 Ω V m k› ‹cN = C M2 M1 Ω V m (Suc k)› by auto
next
case (Suc nat)
then have "TS M2 M1 Ω V m (Suc k) = TS M2 M1 Ω V m k ∪ C M2 M1 Ω V m (Suc k)"
using TS.simps(3) by blast
moreover have "tsN ∪ cN = TS M2 M1 Ω V m k ∪ C M2 M1 Ω V m (Suc k)"
using ‹tsN = TS M2 M1 Ω V m k› ‹cN = C M2 M1 Ω V m (Suc k)› by auto
ultimately show ?thesis
by auto
qed
then have tsN_calc : "tsN ∪ cN = TS M2 M1 Ω V m iter"
using ‹iter = Suc k› by presburger
have cN_calc : "append_set
(cN -
{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN) =
C M2 M1 Ω V m (iter + 1)"
proof -
have "append_set
(cN -
{xs' ∈ cN.
¬ io_reduction_on M1 {xs'} M2 ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN) =
append_set
((C M2 M1 Ω V m iter) -
(RM M2 M1 Ω V m iter))
(inputs M2) -
(TS M2 M1 Ω V m iter) "
using ‹cN = C M2 M1 Ω V m iter› ‹tsN ∪ cN = TS M2 M1 Ω V m iter› rmN_calc by presburger
moreover have "append_set
((C M2 M1 Ω V m iter) -
(RM M2 M1 Ω V m iter))
(inputs M2) -
(TS M2 M1 Ω V m iter) = C M2 M1 Ω V m (iter + 1)"
proof -
have "C M2 M1 Ω V m (iter + 1) = C M2 M1 Ω V m ((Suc k) + 1)"
using ‹iter = Suc k› by presburger+
moreover have "(Suc k) + 1 = Suc (Suc k)"
by simp
ultimately have "C M2 M1 Ω V m (iter + 1) = C M2 M1 Ω V m (Suc (Suc k))"
by presburger
have "C M2 M1 Ω V m (Suc (Suc k))
= append_set (C M2 M1 Ω V m (Suc k) - RM M2 M1 Ω V m (Suc k)) (inputs M2)
- TS M2 M1 Ω V m (Suc k)"
using C.simps(3)[of M2 M1 Ω V m k] by linarith
show ?thesis
using Suc_eq_plus1
‹C M2 M1 Ω V m (Suc (Suc k))
= append_set (C M2 M1 Ω V m (Suc k) - RM M2 M1 Ω V m (Suc k)) (inputs M2)
- TS M2 M1 Ω V m (Suc k)›
‹iter = Suc k›
by presburger
qed
ultimately show ?thesis
by presburger
qed
have obs_calc : "obs ∪
L⇩i⇩n M2
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)) =
L⇩i⇩n M2
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)))"
proof -
have "⋀A. L⇩i⇩n M2 (tsN ∪ cN ∪ A) = obs ∪ L⇩i⇩n M2 A"
by (metis (no_types) language_state_for_inputs_union precond)
then show ?thesis
by blast
qed
have obsI_calc : "obsI ∪
L⇩i⇩n M1
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)) =
L⇩i⇩n M1
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)))"
proof -
have "⋀A. L⇩i⇩n M1 (tsN ∪ cN ∪ A) = obsI ∪ L⇩i⇩n M1 A"
by (metis (no_types) language_state_for_inputs_union precond)
then show ?thesis
by blast
qed
have obs⇩Ω_calc : "obs⇩Ω ∪
(⋃io∈L⇩i⇩n M2
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)).
{io} × B M2 io Ω) =
(⋃io∈L⇩i⇩n M2
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))).
{io} × B M2 io Ω)"
using ‹obs = L⇩i⇩n M2 (tsN ∪ cN)›
‹obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)›
obs_calc
by blast
have obsI⇩Ω_calc : "obsI⇩Ω ∪
(⋃io∈L⇩i⇩n M1
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)).
{io} × B M1 io Ω) =
(⋃io∈L⇩i⇩n M1
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))).
{io} × B M1 io Ω)"
using ‹obsI = L⇩i⇩n M1 (tsN ∪ cN)›
‹obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)›
obsI_calc
by blast
have "0 < iter + 1"
using ‹0 < iter› by simp
have "tsN ∪ cN = TS M2 M1 Ω V m (iter + 1 - 1)"
using tsN_calc by simp
from ‹0 < iter + 1›
‹tsN ∪ cN = TS M2 M1 Ω V m (iter + 1 - 1)›
cN_calc
rmN_calc'
obs_calc
obsI_calc
obs⇩Ω_calc
obsI⇩Ω_calc
‹OFSM M1›
‹OFSM M2›
‹asc_fault_domain M2 M1 m›
‹test_tools M2 M1 FAIL PM V Ω›
show "0 < iter + 1 ∧
tsN ∪ cN = TS M2 M1 Ω V m (iter + 1 - 1) ∧
append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN) =
C M2 M1 Ω V m (iter + 1) ∧
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''. ∀io2∈RP M2 s2 vs xs V''.
B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')} =
RM M2 M1 Ω V m (iter + 1 - 1) ∧
obs ∪
L⇩i⇩n M2
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)) =
L⇩i⇩n M2
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))) ∧
obsI ∪
L⇩i⇩n M1
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)) =
L⇩i⇩n M1
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))) ∧
obs⇩Ω ∪
(⋃io∈L⇩i⇩n M2
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)).
{io} × B M2 io Ω) =
(⋃io∈L⇩i⇩n M2
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))).
{io} × B M2 io Ω) ∧
obsI⇩Ω ∪
(⋃io∈L⇩i⇩n M1
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN)).
{io} × B M1 io Ω) =
(⋃io∈L⇩i⇩n M1
(tsN ∪ cN ∪
(append_set
(cN -
{xs' ∈ cN.
¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'} ∨
(∀io∈L⇩i⇩n M1 {xs'}.
∃V''∈N io M1 V.
∃S1 vs xs.
io = vs @ xs ∧
mcp (vs @ xs) V'' vs ∧
S1 ⊆ nodes M2 ∧
(∀s1∈S1.
∀s2∈S1.
s1 ≠ s2 ⟶
(∀io1∈RP M2 s1 vs xs V''.
∀io2∈RP M2 s2 vs xs V''. B M1 io1 Ω ≠ B M1 io2 Ω)) ∧
m < LB M2 M1 vs xs (tsN ∪ V) S1 Ω V'')})
(inputs M2) -
(tsN ∪ cN))).
{io} × B M1 io Ω) ∧
OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω"
by linarith
next
fix tsN cN rmN obs obsI obs⇩Ω obsI⇩Ω iter isReduction
assume precond : "(0 < iter ∧
tsN = TS M2 M1 Ω V m (iter - 1) ∧
cN = C M2 M1 Ω V m iter ∧
rmN = RM M2 M1 Ω V m (iter - 1) ∧
obs = L⇩i⇩n M2 (tsN ∪ cN) ∧
obsI = L⇩i⇩n M1 (tsN ∪ cN) ∧
obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω) ∧
obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω) ∧
OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω) ∧
¬ (cN ≠ {} ∧ obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω)"
then have "0 < iter"
"OFSM M1"
"OFSM M2"
"asc_fault_domain M2 M1 m"
"test_tools M2 M1 FAIL PM V Ω"
"cN = {} ∨ ¬ obsI ⊆ obs ∨ ¬ obsI⇩Ω ⊆ obs⇩Ω"
"tsN = TS M2 M1 Ω V m (iter-1)"
"cN = C M2 M1 Ω V m iter"
"rmN = RM M2 M1 Ω V m (iter-1)"
"obs = L⇩i⇩n M2 (tsN ∪ cN)"
"obsI = L⇩i⇩n M1 (tsN ∪ cN)"
"obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)"
"obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)"
by linarith+
show "(obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω) = M1 ≼ M2"
proof (cases "cN = {}")
case True
then have "C M2 M1 Ω V m iter = {}"
using ‹cN = C M2 M1 Ω V m iter› by auto
have "is_det_state_cover M2 V"
using ‹test_tools M2 M1 FAIL PM V Ω› by auto
then have "[] ∈ V"
using det_state_cover_initial[of M2 V] by simp
then have "V ≠ {}"
by blast
have "Suc 0 < iter"
proof (rule ccontr)
assume "¬ Suc 0 < iter"
then have "iter = Suc 0"
using ‹0 < iter› by auto
then have "C M2 M1 Ω V m (Suc 0) = {}"
using ‹C M2 M1 Ω V m iter = {}› by auto
moreover have "C M2 M1 Ω V m (Suc 0) = V"
by auto
ultimately show"False"
using ‹V ≠ {}› by blast
qed
obtain k where "iter = Suc k"
using gr0_implies_Suc[OF ‹0 < iter›] by blast
then have "Suc 0 < Suc k"
using ‹Suc 0 < iter› by auto
then have "0 < k"
by simp
then obtain k' where "k = Suc k'"
using gr0_implies_Suc by blast
have "iter = Suc (Suc k')"
using ‹iter = Suc k› ‹k = Suc k'› by simp
have "TS M2 M1 Ω V m (Suc (Suc k')) = TS M2 M1 Ω V m (Suc k') ∪ C M2 M1 Ω V m (Suc (Suc k'))"
using TS.simps(3)[of M2 M1 Ω V m k'] by blast
then have "TS M2 M1 Ω V m iter = TS M2 M1 Ω V m (Suc k')"
using True ‹cN = C M2 M1 Ω V m iter› ‹iter = Suc (Suc k')› by blast
moreover have "Suc k' = iter - 1"
using ‹iter = Suc (Suc k')› by presburger
ultimately have "TS M2 M1 Ω V m iter = TS M2 M1 Ω V m (iter - 1)"
by auto
then have "tsN = TS M2 M1 Ω V m iter"
using ‹tsN = TS M2 M1 Ω V m (iter-1)› by simp
then have "TS M2 M1 Ω V m iter = TS M2 M1 Ω V m (iter - 1)"
using ‹tsN = TS M2 M1 Ω V m (iter - 1)› by auto
then have "final_iteration M2 M1 Ω V m (iter-1)"
using ‹0 < iter› by auto
have "M1 ≼ M2 = atc_io_reduction_on_sets M1 tsN Ω M2"
using asc_main_theorem[OF ‹OFSM M1› ‹OFSM M2›
‹asc_fault_domain M2 M1 m›
‹test_tools M2 M1 FAIL PM V Ω›
‹final_iteration M2 M1 Ω V m (iter-1)›]
using ‹tsN = TS M2 M1 Ω V m (iter - 1)›
by blast
moreover have "tsN ∪ cN = tsN"
using ‹cN = {}› by blast
ultimately have "M1 ≼ M2 = atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
by presburger
have "obsI ⊆ obs ≡ L⇩i⇩n M1 (tsN ∪ cN) ⊆ L⇩i⇩n M2 (tsN ∪ cN)"
by (simp add: ‹obs = L⇩i⇩n M2 (tsN ∪ cN)› ‹obsI = L⇩i⇩n M1 (tsN ∪ cN)›)
have "obsI⇩Ω ⊆ obs⇩Ω ≡ (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)
⊆ (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)"
by (simp add: ‹obsI⇩Ω = (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)›
‹obs⇩Ω = (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)›)
have "(obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω) = atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
proof
assume "obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω"
show "atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
using atc_io_reduction_on_sets_from_obs[of M1 "tsN ∪ cN" M2 Ω]
using ‹obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω› ‹obsI ⊆ obs ≡ L⇩i⇩n M1 (tsN ∪ cN) ⊆ L⇩i⇩n M2 (tsN ∪ cN)›
‹obsI⇩Ω ⊆ obs⇩Ω ≡ (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)
⊆ (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)›
by linarith
next
assume "atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
show "obsI ⊆ obs ∧ obsI⇩Ω ⊆ obs⇩Ω"
using atc_io_reduction_on_sets_to_obs[of M1 ‹tsN ∪ cN› Ω M2]
‹atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2›
‹obsI ⊆ obs ≡ L⇩i⇩n M1 (tsN ∪ cN) ⊆ L⇩i⇩n M2 (tsN ∪ cN)›
‹obsI⇩Ω ⊆ obs⇩Ω ≡ (⋃io∈L⇩i⇩n M1 (tsN ∪ cN). {io} × B M1 io Ω)
⊆ (⋃io∈L⇩i⇩n M2 (tsN ∪ cN). {io} × B M2 io Ω)›
by blast
qed
then show ?thesis
using ‹M1 ≼ M2 = atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2› by linarith
next
case False
then have "¬ obsI ⊆ obs ∨ ¬ obsI⇩Ω ⊆ obs⇩Ω"
using ‹cN = {} ∨ ¬ obsI ⊆ obs ∨ ¬ obsI⇩Ω ⊆ obs⇩Ω› by auto
have "¬ atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
using atc_io_reduction_on_sets_to_obs[of M1 "tsN ∪ cN" Ω M2]
‹¬ obsI ⊆ obs ∨ ¬ obsI⇩Ω ⊆ obs⇩Ω› precond
by fastforce
have "¬ M1 ≼ M2"
proof
assume "M1 ≼ M2"
have "atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2"
using asc_soundness[OF ‹OFSM M1› ‹OFSM M2›] ‹M1 ≼ M2› by blast
then show "False"
using ‹¬ atc_io_reduction_on_sets M1 (tsN ∪ cN) Ω M2› by blast
qed
then show ?thesis
using ‹¬ obsI ⊆ obs ∨ ¬ obsI⇩Ω ⊆ obs⇩Ω› by blast
qed
qed
end