Theory Simulation_Graphs2
section ‹Simulations for Buechi Properties›
theory Simulation_Graphs2
imports Timed_Automata.Simulation_Graphs "HOL-Eisbach.Eisbach"
begin
text ‹
This theory essentially formalizes the concepts from Guangyuan Li's FORMATS 2009 paper
``Checking Timed Büchi Automata Emptiness Using LU-Abstractions'' \<^cite>‹"Li:FORMATS:2009"›.
However, instead of formalizing this directly for the notions of timed Büchi automata,
time-abstract simulations, and zone graphs with abstractions,
we use general notions of simulation graphs with certain properties.
›
subsection ‹Misc›
lemma map_eq_append_conv:
"(map f xs = ys @ zs) = (∃as bs. xs = as @ bs ∧ map f as = ys ∧ map f bs = zs)"
by (induction ys arbitrary: xs; simp add: map_eq_Cons_conv; metis append_Cons)
lemma Cons_subseq_iff:
"subseq (x # xs) ys ⟷ (∃as bs. ys = as @ x # bs ∧ subseq xs bs)"
using list_emb_ConsD list_emb_append2 by fastforce
lemma append_subseq_iff:
"subseq (as @ bs) xs ⟷ (∃ys zs. xs = ys @ zs ∧ subseq as ys ∧ subseq bs zs)"
by (meson list_emb_appendD list_emb_append_mono)
context Graph_Defs
begin
lemma steps_append_singleE:
assumes "steps (xs @ [x])"
obtains "xs = []" | ys y where "xs = ys @ [y]" "steps xs" "y → x"
using assms by (metis append_butlast_last_id list.distinct(1) list.sel(1) steps_decomp)
lemma steps_alt_induct2[consumes 1, case_names Single Snoc]:
assumes
"steps (a # xs @ [b])" "(⋀b. E a b ⟹ P a [] b)"
"⋀y x xs. E y x ⟹ steps (a # xs @ [y]) ⟹ P a xs y ⟹ P a (xs @ [y]) x"
shows "P a xs b"
using assms(1)
apply (induction "a # xs @ [b]" arbitrary: xs b rule: steps_alt_induct)
subgoal
apply auto
done
subgoal for y x xs ys b
apply (cases "ys = []")
apply (force intro: assms(2); fail)
apply (simp, metis append.simps(2) append1_eq_conv append_butlast_last_id assms(3))
done
done
lemma steps_singleI:
"steps [a,b]" if "a → b"
using that steps.intros by blast
end
subsection ‹Backward Simulations›
locale Backward_Simulation = Simulation where A = E and B = E and sim = sim
for E :: "'a ⇒ 'a ⇒ bool" and sim (infix "≼" 60) +
fixes G :: "'a set ⇒ 'a set ⇒ bool"
assumes simulation: "b ∈ B ⟹ G A B ⟹ ∃a ∈ A. ∃b'. a → b' ∧ b ≼ b'"
and refl[intro, simp]: "a ≼ a" and trans: "transp (≼)"
begin
lemmas A_simulation_steps = simulation_steps
sublocale Graph_Defs G .
lemmas sim_transD[intro] = transpD[OF trans]
lemma backward_simulation_reaches:
"∃a ∈ A. ∃b'. E⇧*⇧* a b' ∧ b ≼ b'" if "G⇧*⇧* A B" "b ∈ B"
using that
proof (induction arbitrary: b rule: rtranclp_induct)
case base
then show ?case
by auto
next
case (step Y Z)
from simulation[OF ‹b ∈ Z› ‹G Y Z›] obtain a b' where "a ∈ Y" "a → b'" "b ≼ b'"
by safe
from step.IH[OF ‹a ∈ Y›] obtain a0 a' where "a0 ∈ A" "a0 →* a'" "a ≼ a'"
by safe
moreover from A_B_step[OF ‹a → b'› ‹a ≼ a'›] obtain b'' where "a' → b''" "b' ≼ b''"
by safe
with ‹a0 ∈ A› ‹a0 →* a'› ‹b ≼ b'› show ?case
by (auto intro: rtranclp.intros(2))
qed
lemma backward_simulation_steps:
"∃a ∈ A. ∃as b'. A.steps (a # as @ [b']) ∧ b ≼ b'" if "steps (A # As @ [B])" "b ∈ B"
using that
proof (induction A As B arbitrary: b rule: steps_alt_induct2)
case (Single x)
from simulation[OF this(2,1)] show ?case
by (safe, intro bexI exI[where x = "[]"]) auto
next
case (Snoc B C As c)
from simulation[OF ‹c ∈ C› ‹G B C›] obtain b c' where "b ∈ B" "b → c'" "c ≼ c'"
by safe
with Snoc.IH obtain a as b' where "a ∈ A" "A.steps (a # as @ [b'])" "b ≼ b'"
by blast
moreover from ‹b ≼ b'› ‹b → c'› obtain c'' where "b' → c''" "c' ≼ c''"
by (auto dest: A_B_step)
ultimately have "a ∈ A" "c ≼ c''" "A.steps (a # (as @ [b']) @ [c''])"
using ‹c ≼ c'› by auto (metis A.steps_appendI append_Cons)
then show ?case
by blast
qed
lemma backward_simulation_reaches1:
"∃a ∈ A. ∃b'. E⇧+⇧+ a b' ∧ b ≼ b'" if "G⇧+⇧+ A B" "b ∈ B"
using that unfolding A.reaches1_steps_iff reaches1_steps_iff
by (auto dest!: backward_simulation_steps)
text ‹Corresponds to lemma 8 of \<^cite>‹"Li:FORMATS:2009"›.›
lemma steps_repeat:
assumes "steps (A # As @ [A])" "a ∈ A" "∀a ∈ A. P a" "∀x y. x ≼ y ∧ x ∈ A ∧ P x ⟶ P y"
obtains x y as xs where
"subseq as xs" "list_all P as" "A.steps (x # xs @ [y])" "length as = n" "a ≼ y" "x ∈ A"
using ‹a ∈ A›
proof (atomize_elim, induction n arbitrary: a)
case 0
from backward_simulation_steps[OF ‹steps (A # As @ [A])› ‹a ∈ A›] obtain a' as b where
"a' ∈ A" "A.steps (a' # as @ [b])" "a ≼ b"
by auto
then show ?case
by (auto 4 4 intro: exI[where x = "[]"])
next
case (Suc n b)
from backward_simulation_steps[OF assms(1) ‹b ∈ A›] obtain a as b' where
"a ∈ A" "A.steps (a # as @ [b'])" "b ≼ b'"
by auto
from Suc.IH[OF ‹a ∈ A› ‹a ∈ A›] obtain as' xs x y where
"subseq as' xs" "list_all P as'" "A.steps (x # xs @ [y])" "n = length as'" "a ≼ y" "x ∈ A"
by auto
moreover from A_simulation_steps[OF ‹A.steps (a # _)› ‹a ≼ y›] ‹b ≼ b'› obtain b'' bs where
"A.steps (y # bs @ [b''])" "list_all2 (≼) as bs" "b ≼ b''"
unfolding list_all2_append1 list_all2_Cons1 by auto
ultimately show ?case
using assms(3,4) ‹a ∈ A›
by (inst_existentials "as' @ [y]" "xs @ [y] @ bs" x b'')
(auto simp: list_emb_append_mono, metis A.steps_append2 append_Cons)
qed
end
subsection ‹Self Simulation for a Finite Simulation Relation›
text ‹
This section makes the following abstractions:
▪ The timed automata semantics correspond to the transition system ‹→› (‹E›).
▪ The finite time-abstract bisimulation ‹≡⇩M› from the classic region construction
corresponds to the simulation ‹≼›.
›
locale Self_Simulation =
Simulation_Invariant where A = E and B = E and sim = sim and PA = P and PB = P
for E :: "'a ⇒ 'a ⇒ bool" and sim (infix "≼" 60) and P +
assumes refl: "reflp (≼)" and trans: "transp (≼)"
begin
lemma sim_reflI[intro, simp]:
"x ≼ x"
using refl unfolding reflp_def by auto
lemmas sim_transD[intro] = transpD[OF trans]
text ‹Corresponds to lemma 3 of \<^cite>‹"Li:FORMATS:2009"›.›
lemma pre_cycle_infinite_cycle:
assumes "A.steps (x # xs @ [y])" "x ≼ y" "P x" "P y"
obtains w where
"A.run (x ## w)" "stream_all2 (≼) (cycle (x # xs)) (x ## w)"
proof -
let ?R = "λa b. a ≼ b ∧ P a ∧ P b"
define nxt where
"nxt ≡ λ(xs, y). SOME (ys, z). A.steps (y # ys @ [z]) ∧ list_all2 ?R xs ys ∧ y ≼ z"
have *: "A.steps (y # ys @ [z]) ∧ list_all2 ?R xs ys ∧ y ≼ z"
if "nxt (xs, y) = (ys, z)" "A.steps(x # xs @ [y])" "x ≼ y" "P x" "P y" for x y xs ys z
proof -
from simulation_steps[OF that(2) ‹x ≼ y›] ‹P x› ‹P y› obtain ws y' where
"A.steps (y # ws @ [y'])" "list_all2 ?R xs ws" "y ≼ y'"
by (smt (z3) list_all2_Cons1 list_all2_Nil list_all2_append1)
then show ?thesis
using ‹nxt _ = _› unfolding nxt_def by (auto dest!: alethe_sko_ex_indirect[OF sym])
qed
let ?w = "flat (smap (λ(xs, y). xs @ [y]) (siterate nxt (xs, y)))"
from assms have "A.run ?w"
proof (coinduction arbitrary: x xs y rule: A.run_flat_coinduct)
case (run_shift as bs xss x xs y)
obtain ys z where "nxt (xs, y) = (ys, z)"
by (cases "nxt (xs, y)")
with run_shift have "as = xs @ [y]" "bs = ys @ [z]"
"bs ## xss = smap (λ(xs, y). xs @ [y]) (siterate nxt (ys, z))"
by auto
with *[OF ‹nxt _ = _› ‹A.steps (x # _)› ‹x ≼ y›] run_shift(2-) show ?case
by (inst_existentials ys z)
(auto 4 3 dest: A.steps_ConsD PA_invariant.invariant_steps elim: A.steps.cases)
qed
with assms(1) have "A.run (x ## ?w)"
apply -
apply (cases "smap (λ(xs, y). xs @ [y]) (siterate nxt (xs, y))")
apply (simp only:)
apply clarsimp
by (smt (z3) A.run.cases A.run.intros A.steps.cases shift_simps(1) stream.sel(1)
append_Nil append_is_Nil_conv hd_append2 list.distinct(1) list.sel)
obtain x' xs' where eqs: "xs = xs'" "x = x'"
by auto
with assms have "A.steps (x' # xs' @ [y])" "list_all2 (≼) xs xs'" "x ≼ x'" "x' ≼ y" "P x'" "P y"
by (auto simp: zip_same list_all2_iff)
then have "stream_all2 (≼) (cycle (xs @ [x])) ?w"
proof (rewrite in ‹(xs, y)› eqs, coinduction arbitrary: x' xs' y rule: stream_rel_coinduct_shift)
case stream_rel
obtain ys z where "nxt (xs', y) = (ys, z)"
by (cases "nxt (xs', y)")
with stream_rel show ?case
apply -
apply (frule (4) *)
apply (inst_existentials "xs @ [x]" "cycle (xs @ [x])" "xs' @ [y]"
"flat (smap (λ(xs, y). xs @ [y]) (siterate nxt (ys, z)))")
subgoal
by simp
(metis cycle_Cons cycle_decomp cycle_rotated list.distinct(1) list.sel(1) list.sel(3))
subgoal
by (cases "smap (λ(xs, y). xs @ [y]) (siterate nxt (xs', y))") (simp only:, auto)
apply (solves ‹auto simp: list_all2_iff›)+
apply (auto 4 5 elim: list_all2_trans[rotated] dest: PA_invariant.invariant_steps)
done
qed
then have "stream_all2 (≼) (cycle (x # xs)) (x ## ?w)"
by (simp add: cycle_Cons)
with ‹A.run (x ## ?w)› show ?thesis
by (auto intro: that)
qed
end
locale Self_Simulation_Finite =
Simulation_Invariant where A = E and B = E and sim = sim and PA = P and PB = P
for E :: "'a ⇒ 'a ⇒ bool" and sim (infix "≼" 60) and P +
assumes equiv_sim: "equivp (≼)" and finite_quotient: "finite (UNIV // {(x, y). x ≼ y})"
begin
sublocale Self_Simulation
apply standard
using equiv_sim apply (simp add: equivp_reflp_symp_transp)+
done
text ‹Roughly corresponds to lemmas 9, 10, and 11 of \<^cite>‹"Li:FORMATS:2009"›.›
lemma steps_cycle_run:
assumes "A.steps (x # xs)" "subseq as xs" "P x" "length as > card (UNIV // {(x, y). x ≼ y})"
"∀x ∈ set as. φ x" "∀x ∈ set as. ∀y. x ≼ y ∧ φ x ⟶ φ y"
obtains w where "A.run (x ## w)" "infs φ w"
proof -
from assms(3) obtain a b as' ys cs' where *: "xs = as' @ a # ys @ b # cs'" "a ≼ b" "a ∈ set as"
proof -
let ?f = "λx. {y. x ≼ y}"
let ?as = "map ?f as"
have "card (set ?as) ≤ card (UNIV // {(x, y). x ≼ y})"
using quotientI[of _ _ "{(x, y). x ≼ y}"]
by (auto intro: finite_quotient surj_card_le[where f = id])
also have "… < length as"
by (rule assms)
finally have "card (set ?as) < length ?as"
by simp
then have "¬ distinct ?as"
using distinct_card[of ?as] by auto
then obtain a b as' ys cs' where "as = as' @ a # ys @ b # cs'" "a ≼ b"
using that
by (clarsimp simp: map_eq_append_conv map_eq_Cons_conv dest!: not_distinct_decomp) blast
then show ?thesis
using that[where a = a and b = b] ‹subseq as xs›
by (simp add: append_subseq_iff Cons_subseq_iff) (metis append.assoc)
qed
have "A.steps (x # as' @ [a])" "A.steps (a # ys @ [b])"
proof -
from assms(1) * show "A.steps (x # as' @ [a])"
using A.steps_appendD1 by auto
from * have "as' @ (a # ys) @ b # cs' = xs"
by simp
have "b # cs' ≠ [] ∧ a # ys ≠ [] ∨ (a # ys) @ b # cs' ≠ [] ∧ ¬ A.steps ((a # ys) @ b # cs')
∨ A.steps ((a # ys) @ [b])"
by blast
with ‹_ = xs› assms(1) have "A.steps ((a # ys) @ [b])"
by (metis (no_types) A.Single A.steps_ConsD A.steps_append_single A.steps_decomp
Nil_is_append_conv list.sel(1) self_append_conv2)
then show "A.steps (a # ys @ [b])"
by simp
qed
with ‹P x› have "P a" "P b"
by (auto 4 3 dest: PA_invariant.invariant_steps)
from pre_cycle_infinite_cycle[OF ‹A.steps (a # ys @ [b])› ‹a ≼ b› this] obtain w where
"A.run (a ## w)" "stream_all2 (≼) (cycle (a # ys)) (a ## w)" .
from this(2) have "infs ((≼) a) (a ## w)"
by (smt (z3) alw_ev_lockstep infs_cycle list.distinct(1) list.set_intros(1) sim_reflI sim_transD)
then have "infs φ (as' @- a ## w)"
using assms(5) ‹a ∈ set as› unfolding ‹xs = as' @ _› apply simp
using assms(6) by (elim infs_mono[rotated]) blast
moreover from ‹A.run _› ‹A.steps (x # as' @ [a])› have "A.run (x ## as' @- a ## w)"
by (metis A.extend_run A.steps_decomp append_Cons list.distinct(1) list.sel(1,3)
shift_simps stream.exhaust stream.sel)
ultimately show ?thesis
by (rule that[rotated])
qed
end
subsection ‹Combining Finite Simulation with Backward Simulation›
text ‹Here, ‹≼› is any time-abstract simulation ‹≼›, and ‹≼'› corresponds to ‹≡⇩M›.›
locale Backward_Double_Simulation = Backward_Simulation where E = E and sim = sim +
finite: Self_Simulation_Finite where E = E and sim = sim'
for E :: "'a ⇒ 'a ⇒ bool" and sim (infix "≼" 60) and sim' (infix "≼''" 60)
begin
text ‹Corresponds to lemma 12 of \<^cite>‹"Li:FORMATS:2009"›.›
lemma cycle_Buechi_run:
assumes "steps (A # As @ [A])" "a ∈ A" "∀a ∈ A. P a" "∀a ∈ A. φ a"
"∀x y. x ≼ y ∧ x ∈ A ∧ φ x ⟶ φ y" "∀x y. x ≼' y ∧ φ x ⟶ φ y"
obtains x xs where "A.run (x ## xs)" "infs φ xs" "x ∈ A"
proof -
let ?n = "card (UNIV // {(x, y). x ≼' y}) + 1"
from steps_repeat[OF assms(1,2,4-5), where n = ?n] obtain x y as ys where *:
"subseq as ys" "list_all φ as" "A.steps (x # ys @ [y])"
"length as = ?n" "a ≼ y" "x ∈ A" .
with assms(4) have "∀x ∈ set as. φ x"
by (auto simp: list_all_iff)
with * assms(3,6) obtain w where "A.run (x ## w)" "infs φ w"
by - (erule finite.steps_cycle_run[where φ = φ], auto)
then show ?thesis
using ‹x ∈ A› by (elim that) simp
qed
end
lemma (in Simulation_Invariant) simulation_run':
assumes "A.run (x ## xs)" "x ∼ y" "PA x" "PB y"
shows "∃ys. B.run (y ## ys) ∧ stream_all2 (λa b. a ∼ b ∧ PA a ∧ PB b) xs ys"
using simulation_run assms unfolding equiv'_def by blast
context Graph_Invariant_Start
begin
lemma reachable_reaches_equiv: "G'.reaches x y ⟷ x →* y" if "reachable x" for x y
using invariant_reaches invariant_reaches_iff reachable_def that by auto
lemma reachable_reaches1_equiv: "G'.reaches1 x y ⟷ x →⇧+ y" if "reachable x" for x y
using invariant_reaches invariant_reaches1_iff reachable_def that by auto
lemma reachable_steps_equiv:
"G'.steps (x # xs) ⟷ steps (x # xs)" if "reachable x"
using invariant_reaches invariant_steps_iff reachable_def that by auto
lemma reachable_run_equiv:
"G'.run (x ## xs) ⟷ run (x ## xs)" if "reachable x"
by (metis reaches_steps_iff Graph_Invariant.invariant_run Graph_Invariant_axioms
invariant_reaches reachable_steps subgraph_run_iff that)
lemmas invariant_subgraph_equivs =
reachable_reaches_equiv reachable_reaches1_equiv reachable_steps_equiv reachable_run_equiv
end
text ‹Adding the assumption that the abstracted zone graph is finite and complete.›
locale Backward_Double_Simulation_Complete =
A: Graph_Defs E + G: Graph_Defs G + G_inv: Graph_Defs "λx y. G x y ∧ Q x ∧ Q y" +
backward: Backward_Double_Simulation where E = E and G = "λx y. G x y ∧ Q x ∧ Q y" +
complete: Simulation_Invariant where A = E and B = G and PA = P and PB = Q and sim = "(∈)" +
Finite_Graph where E = G and x⇩0 = a⇩0 +
Graph_Invariant where E = G and P = Q
for E :: "'a ⇒ 'a ⇒ bool" and G :: "'a set ⇒ 'a set ⇒ bool" and a⇩0 and Q +
assumes Q_P: "Q a ⟹ ∀x ∈ a. P x" and a⇩0_invariant: "Q a⇩0"
begin
sublocale G: Graph_Invariant_Start where E = G and P = Q and s⇩0 = a⇩0
by (standard) (rule a⇩0_invariant)
lemmas G_invariant_subgraph_equivs =
G.invariant_subgraph_equivs[unfolded complete.PB_invariant.E'_def]
text ‹Corresponds to theorem 1 of \<^cite>‹"Li:FORMATS:2009"›.›
theorem Buechi_run_lasso_iff:
assumes
"∀x y. x ≼' y ∧ φ x ⟶ φ y"
"∀x y. x ≼ y ∧ φ x ⟶ φ y"
"∀x y A. G.reaches a⇩0 A ∧ x ∈ A ∧ y ∈ A ∧ φ x ⟶ φ y"
shows
"(∃x⇩0 xs. x⇩0 ∈ a⇩0 ∧ A.run (x⇩0 ## xs) ∧ infs φ (x⇩0 ## xs))
⟷ (∃as a bs. G.steps (a⇩0 # as @ a # bs @ [a]) ∧ (∀x ∈ a. φ x) ∧ a ≠ {})"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain x⇩0 xs where "x⇩0 ∈ a⇩0" "A.run (x⇩0 ## xs)" "infs φ xs"
by auto
have backward_reaches_A: "G.reaches a⇩0 A" if "G_inv.reaches a⇩0 A" for A
using that by (simp add: G_invariant_subgraph_equivs[symmetric])
from complete.simulation_run'[OF ‹A.run _› ‹x⇩0 ∈ _›] a⇩0_invariant ‹x⇩0 ∈ a⇩0› obtain as where
"G.run (a⇩0 ## as)" "stream_all2 (λa b. a ∈ b ∧ P a ∧ Q b) xs as"
by (auto dest: Q_P)
from ‹G.run (a⇩0 ## as)› have "G_inv.run (a⇩0 ## as)"
by (simp add: G_invariant_subgraph_equivs)
from ‹infs φ _› ‹stream_all2 _ _ _› have "infs (λa. ∃x ∈ a. φ x) as"
by (rule alw_ev_lockstep) fast
then have "infs (λa. (∀x ∈ a. φ x) ∧ a ≠ {}) as"
using assms(3) ‹G_inv.run (a⇩0 ## as)›
by (auto 4 5 simp: stream.pred_set dest!: G_inv.run_reachable backward_reaches_A
elim!: infs_mono[rotated])
with ‹G.run _› show ?rhs
apply -
apply (erule buechi_run_lasso)
apply (simp; fail)
by (metis (lifting)
G.reaches1_steps_append G.reaches1_steps_iff G.reaches_stepsE G.steps_reaches1 list.sel(1))
next
assume ?rhs
then obtain as a x bs where "G.steps (a⇩0 # as @ a # bs @ [a])" "∀x ∈ a. φ x" "x ∈ a"
by auto
then have "G.reaches a⇩0 a" "G.reaches1 a⇩0 a"
apply -
subgoal A
by (smt (z3) G.steps_reaches append_Cons last_appendR last_snoc list.sel(1))
subgoal
by (metis A G.steps_ConsD G.steps_appendD2 G.steps_reaches1
append_is_Nil_conv list.distinct(1) rtranclpD)
done
moreover from ‹G.steps (a⇩0 # as @ a # bs @ [a])› have "G.steps (a # bs @ [a])"
by (metis append_is_Nil_conv list.distinct(1) G.steps_ConsD G.steps_appendD2)
ultimately have "G_inv.reaches1 a⇩0 a" "G_inv.steps (a # bs @ [a])"
by (simp add: G_invariant_subgraph_equivs G.reachable_def)+
from ‹G.reaches a⇩0 a› a⇩0_invariant have "Q a"
by (rule complete.PB_invariant.invariant_reaches)
with assms(1,2) ‹G.reaches _ _› ‹∀x ∈ a. φ x› obtain x xs where
"A.run (x ## xs)" "infs φ xs" "x ∈ a"
by - (rule backward.cycle_Buechi_run[OF ‹G_inv.steps (a # bs @ [a])› ‹x ∈ a›, where φ = φ],
(blast dest: Q_P)+)
from backward.backward_simulation_reaches1[OF ‹G_inv.reaches1 a⇩0 a› ‹x ∈ a›] obtain x⇩0 x' where
"x⇩0 ∈ a⇩0" "x ≼ x'" "x⇩0 →⇧+ x'"
by auto
then obtain ys where "A.steps (x⇩0 # ys @ [x'])"
using A.reaches1_steps_iff by auto
from backward.simulation_run[OF ‹A.run _› ‹x ≼ x'›] obtain xs' where
"A.run (x' ## xs')" "stream_all2 (≼) xs xs'"
by (elim conjE exE)
with ‹A.steps _› have "A.run (x⇩0 ## ys @- x' ## xs')"
by (metis A.extend_run A.steps_decomp
append_Cons list.distinct(1) list.sel(1,3) shift_simps(1,2) stream.collapse)
moreover from ‹infs _ _› ‹stream_all2 _ _ _› assms(2) have "infs φ xs'"
by (auto elim!: alw_ev_lockstep)
ultimately show ?lhs
using ‹x⇩0 ∈ a⇩0› by auto
qed
end
end