theory QuotScript+ −
imports Main+ −
begin+ −
+ −
definition + −
"EQUIV E \<equiv> \<forall>x y. E x y = (E x = E y)" + −
+ −
definition+ −
"REFL E \<equiv> \<forall>x. E x x"+ −
+ −
definition + −
"SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"+ −
+ −
definition+ −
"TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"+ −
+ −
lemma EQUIV_REFL_SYM_TRANS:+ −
shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)"+ −
unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq+ −
by (blast)+ −
+ −
lemma EQUIV_REFL:+ −
shows "EQUIV E ==> REFL E"+ −
by (simp add: EQUIV_REFL_SYM_TRANS)+ −
+ −
definition+ −
"PART_EQUIV E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"+ −
+ −
lemma EQUIV_IMP_PART_EQUIV:+ −
assumes a: "EQUIV E"+ −
shows "PART_EQUIV E"+ −
using a unfolding EQUIV_def PART_EQUIV_def+ −
by auto+ −
+ −
definition+ −
"QUOTIENT E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> + −
(\<forall>a. E (Rep a) (Rep a)) \<and> + −
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"+ −
+ −
lemma QUOTIENT_ABS_REP:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "Abs (Rep a) = a" + −
using a unfolding QUOTIENT_def+ −
by simp+ −
+ −
lemma QUOTIENT_REP_REFL:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "E (Rep a) (Rep a)" + −
using a unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma QUOTIENT_REL:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"+ −
using a unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma QUOTIENT_REL_ABS:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "E r s \<Longrightarrow> Abs r = Abs s"+ −
using a unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma QUOTIENT_REL_ABS_EQ:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"+ −
using a unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma QUOTIENT_REL_REP:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "E (Rep a) (Rep b) = (a = b)"+ −
using a unfolding QUOTIENT_def+ −
by metis+ −
+ −
lemma QUOTIENT_REP_ABS:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"+ −
using a unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma IDENTITY_EQUIV:+ −
shows "EQUIV (op =)"+ −
unfolding EQUIV_def+ −
by auto+ −
+ −
lemma IDENTITY_QUOTIENT:+ −
shows "QUOTIENT (op =) id id"+ −
unfolding QUOTIENT_def id_def+ −
by blast+ −
+ −
lemma QUOTIENT_SYM:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "SYM E"+ −
using a unfolding QUOTIENT_def SYM_def+ −
by metis+ −
+ −
lemma QUOTIENT_TRANS:+ −
assumes a: "QUOTIENT E Abs Rep"+ −
shows "TRANS E"+ −
using a unfolding QUOTIENT_def TRANS_def+ −
by metis+ −
+ −
fun+ −
prod_rel+ −
where+ −
"prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"+ −
+ −
fun+ −
fun_map+ −
where+ −
"fun_map f g h x = g (h (f x))"+ −
+ −
+ −
abbreviation+ −
fun_map_syn (infixr "--->" 55)+ −
where+ −
"f ---> g \<equiv> fun_map f g"+ −
+ −
lemma FUN_MAP_I:+ −
shows "(id ---> id) = id"+ −
by (simp add: expand_fun_eq id_def)+ −
+ −
lemma IN_FUN:+ −
shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"+ −
by (simp add: mem_def)+ −
+ −
fun+ −
FUN_REL + −
where+ −
"FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"+ −
+ −
abbreviation+ −
FUN_REL_syn ("_ ===> _")+ −
where+ −
"E1 ===> E2 \<equiv> FUN_REL E1 E2" + −
+ −
lemma FUN_REL_EQ:+ −
"(op =) ===> (op =) = (op =)"+ −
by (simp add: expand_fun_eq)+ −
+ −
lemma FUN_QUOTIENT:+ −
assumes q1: "QUOTIENT R1 abs1 rep1"+ −
and q2: "QUOTIENT R2 abs2 rep2"+ −
shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"+ −
proof -+ −
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"+ −
apply(simp add: expand_fun_eq)+ −
using q1 q2+ −
apply(simp add: QUOTIENT_def)+ −
done+ −
moreover+ −
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"+ −
apply(auto)+ −
using q1 q2 unfolding QUOTIENT_def+ −
apply(metis)+ −
done+ −
moreover+ −
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> + −
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"+ −
apply(auto simp add: expand_fun_eq)+ −
using q1 q2 unfolding QUOTIENT_def+ −
apply(metis)+ −
using q1 q2 unfolding QUOTIENT_def+ −
apply(metis)+ −
using q1 q2 unfolding QUOTIENT_def+ −
apply(metis)+ −
using q1 q2 unfolding QUOTIENT_def+ −
apply(metis)+ −
done+ −
ultimately+ −
show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"+ −
unfolding QUOTIENT_def by blast+ −
qed+ −
+ −
definition+ −
Respects+ −
where+ −
"Respects R x \<equiv> (R x x)"+ −
+ −
lemma IN_RESPECTS:+ −
shows "(x \<in> Respects R) = R x x"+ −
unfolding mem_def Respects_def by simp+ −
+ −
lemma RESPECTS_THM:+ −
shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"+ −
unfolding Respects_def+ −
by (simp add: expand_fun_eq) + −
+ −
lemma RESPECTS_MP:+ −
assumes a: "Respects (R1 ===> R2) f"+ −
and b: "R1 x y"+ −
shows "R2 (f x) (f y)"+ −
using a b unfolding Respects_def+ −
by simp+ −
+ −
lemma RESPECTS_REP_ABS:+ −
assumes a: "QUOTIENT R1 Abs1 Rep1"+ −
and b: "Respects (R1 ===> R2) f"+ −
and c: "R1 x x"+ −
shows "R2 (f (Rep1 (Abs1 x))) (f x)"+ −
using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def+ −
by blast+ −
+ −
lemma RESPECTS_o:+ −
assumes a: "Respects (R2 ===> R3) f"+ −
and b: "Respects (R1 ===> R2) g"+ −
shows "Respects (R1 ===> R3) (f o g)"+ −
using a b unfolding Respects_def+ −
by simp+ −
+ −
(*+ −
definition+ −
"RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> + −
(\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"+ −
*)+ −
+ −
lemma FUN_REL_EQ_REL:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) + −
\<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"+ −
using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq+ −
by blast+ −
+ −
(* q1 and q2 not used; see next lemma *)+ −
lemma FUN_REL_MP:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"+ −
by simp+ −
+ −
lemma FUN_REL_IMP:+ −
shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"+ −
by simp+ −
+ −
lemma FUN_REL_EQUALS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and r1: "Respects (R1 ===> R2) f"+ −
and r2: "Respects (R1 ===> R2) g" + −
shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"+ −
apply(rule_tac iffI)+ −
using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def+ −
apply(metis FUN_REL_IMP)+ −
using r1 unfolding Respects_def expand_fun_eq+ −
apply(simp (no_asm_use))+ −
apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1])+ −
done+ −
+ −
(* ask Peter: FUN_REL_IMP used twice *) + −
lemma FUN_REL_IMP2:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and r1: "Respects (R1 ===> R2) f"+ −
and r2: "Respects (R1 ===> R2) g" + −
and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"+ −
shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"+ −
using q1 q2 r1 r2 a+ −
by (simp add: FUN_REL_EQUALS)+ −
+ −
lemma EQUALS_PRS:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
shows "(x = y) = R (Rep x) (Rep y)"+ −
by (simp add: QUOTIENT_REL_REP[OF q]) + −
+ −
lemma EQUALS_RSP:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
and a: "R x1 x2" "R y1 y2"+ −
shows "R x1 y1 = R x2 y2"+ −
using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def+ −
using a by blast+ −
+ −
lemma LAMBDA_PRS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))"+ −
unfolding expand_fun_eq+ −
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]+ −
by simp+ −
+ −
lemma LAMBDA_PRS1:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"+ −
unfolding expand_fun_eq+ −
by (subst LAMBDA_PRS[OF q1 q2]) (simp)+ −
+ −
(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)+ −
lemma LAMBDA_RSP:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and a: "(R1 ===> R2) f1 f2"+ −
shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"+ −
by (rule a)+ −
+ −
(* ASK Peter about next four lemmas in quotientScript+ −
lemma ABSTRACT_PRS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "f = (Rep1 ---> Abs2) ???"+ −
*)+ −
+ −
lemma LAMBDA_REP_ABS_RSP:+ −
assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"+ −
and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"+ −
shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"+ −
using r1 r2 by auto+ −
+ −
lemma REP_ABS_RSP:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
and a: "R x1 x2"+ −
shows "R x1 (Rep (Abs x2))"+ −
and "R (Rep (Abs x1)) x2"+ −
proof -+ −
show "R x1 (Rep (Abs x2))" + −
using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])+ −
next+ −
show "R (Rep (Abs x1)) x2"+ −
using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])+ −
qed+ −
+ −
(* ----------------------------------------------------- *)+ −
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)+ −
(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)+ −
(* ----------------------------------------------------- *)+ −
+ −
(* what is RES_FORALL *)+ −
(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>+ −
!f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)+ −
(*as peter here *)+ −
+ −
(* bool theory: COND, LET *)+ −
+ −
lemma IF_PRS:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
shows "If a b c = Abs (If a (Rep b) (Rep c))"+ −
using QUOTIENT_ABS_REP[OF q] by auto+ −
+ −
(* ask peter: no use of q *)+ −
lemma IF_RSP:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
and a: "a1 = a2" "R b1 b2" "R c1 c2"+ −
shows "R (If a1 b1 c1) (If a2 b2 c2)"+ −
using a by auto+ −
+ −
lemma LET_PRS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"+ −
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto+ −
+ −
lemma LET_RSP:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and a1: "(R1 ===> R2) f g"+ −
and a2: "R1 x y"+ −
shows "R2 (Let x f) (Let y g)"+ −
using FUN_REL_MP[OF q1 q2 a1] a2+ −
by auto+ −
+ −
+ −
(* ask peter what are literal_case *)+ −
(* literal_case_PRS *)+ −
(* literal_case_RSP *)+ −
+ −
+ −
(* FUNCTION APPLICATION *)+ −
+ −
lemma APPLY_PRS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"+ −
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto+ −
+ −
(* ask peter: no use of q1 q2 *)+ −
lemma APPLY_RSP:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and a: "(R1 ===> R2) f g" "R1 x y"+ −
shows "R2 (f x) (g y)"+ −
using a by (rule FUN_REL_IMP)+ −
+ −
+ −
(* combinators: I, K, o, C, W *)+ −
+ −
lemma I_PRS:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
shows "id e = Abs (id (Rep e))"+ −
using QUOTIENT_ABS_REP[OF q] by auto+ −
+ −
lemma I_RSP:+ −
assumes q: "QUOTIENT R Abs Rep"+ −
and a: "R e1 e2"+ −
shows "R (id e1) (id e2)"+ −
using a by auto+ −
+ −
lemma o_PRS:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and q3: "QUOTIENT R3 Abs3 Rep3"+ −
shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"+ −
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3]+ −
unfolding o_def expand_fun_eq+ −
by simp+ −
+ −
lemma o_RSP:+ −
assumes q1: "QUOTIENT R1 Abs1 Rep1"+ −
and q2: "QUOTIENT R2 Abs2 Rep2"+ −
and q3: "QUOTIENT R3 Abs3 Rep3"+ −
and a1: "(R2 ===> R3) f1 f2"+ −
and a2: "(R1 ===> R2) g1 g2"+ −
shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"+ −
using a1 a2 unfolding o_def expand_fun_eq+ −
by (auto)+ −
+ −
+ −
(* TODO: Put the following lemmas in proper places *)+ −
+ −
lemma equiv_res_forall:+ −
fixes P :: "'a \<Rightarrow> bool"+ −
assumes a: "EQUIV E"+ −
shows "Ball (Respects E) P = (All P)"+ −
using a by (metis EQUIV_def IN_RESPECTS a)+ −
+ −
lemma equiv_res_exists:+ −
fixes P :: "'a \<Rightarrow> bool"+ −
assumes a: "EQUIV E"+ −
shows "Bex (Respects E) P = (Ex P)"+ −
using a by (metis EQUIV_def IN_RESPECTS a)+ −
+ −
lemma FORALL_REGULAR:+ −
assumes a: "!x :: 'a. (P x --> Q x)"+ −
and b: "All P"+ −
shows "All Q"+ −
using a b by (metis)+ −
+ −
lemma EXISTS_REGULAR:+ −
assumes a: "!x :: 'a. (P x --> Q x)"+ −
and b: "Ex P"+ −
shows "Ex Q"+ −
using a b by (metis)+ −
+ −
lemma RES_FORALL_REGULAR:+ −
assumes a: "!x :: 'a. (R x --> P x --> Q x)"+ −
and b: "Ball R P"+ −
shows "Ball R Q"+ −
using a b by (metis COMBC_def Collect_def Collect_mem_eq)+ −
+ −
lemma RES_EXISTS_REGULAR:+ −
assumes a: "!x :: 'a. (R x --> P x --> Q x)"+ −
and b: "Bex R P"+ −
shows "Bex R Q"+ −
using a b by (metis COMBC_def Collect_def Collect_mem_eq)+ −
+ −
lemma LEFT_RES_FORALL_REGULAR:+ −
assumes a: "!x. (R x \<and> (Q x --> P x))"+ −
shows "Ball R Q ==> All P"+ −
using a+ −
apply (metis COMBC_def Collect_def Collect_mem_eq a)+ −
done+ −
+ −
lemma RIGHT_RES_FORALL_REGULAR:+ −
assumes a: "!x :: 'a. (R x --> P x --> Q x)"+ −
shows "All P ==> Ball R Q"+ −
using a+ −
apply (metis COMBC_def Collect_def Collect_mem_eq a)+ −
done+ −
+ −
lemma LEFT_RES_EXISTS_REGULAR:+ −
assumes a: "!x :: 'a. (R x --> Q x --> P x)"+ −
shows "Bex R Q ==> Ex P"+ −
using a by (metis COMBC_def Collect_def Collect_mem_eq)+ −
+ −
lemma RIGHT_RES_EXISTS_REGULAR:+ −
assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))"+ −
shows "Ex P \<Longrightarrow> Bex R Q"+ −
using a by (metis COMBC_def Collect_def Collect_mem_eq)+ −
+ −
(* TODO: Add similar *)+ −
lemma RES_FORALL_RSP:+ −
shows "\<And>f g. (R ===> (op =)) f g ==>+ −
(Ball (Respects R) f = Ball (Respects R) g)"+ −
apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)+ −
done+ −
+ −
lemma RES_EXISTS_RSP:+ −
shows "\<And>f g. (R ===> (op =)) f g ==>+ −
(Bex (Respects R) f = Bex (Respects R) g)"+ −
apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)+ −
done+ −
+ −
+ −
lemma FORALL_PRS:+ −
assumes a: "QUOTIENT R absf repf"+ −
shows "All f = Ball (Respects R) ((absf ---> id) f)"+ −
using a+ −
unfolding QUOTIENT_def+ −
by (metis IN_RESPECTS fun_map.simps id_apply)+ −
+ −
lemma EXISTS_PRS:+ −
assumes a: "QUOTIENT R absf repf"+ −
shows "Ex f = Bex (Respects R) ((absf ---> id) f)"+ −
using a+ −
unfolding QUOTIENT_def+ −
by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)+ −
+ −
lemma COND_PRS:+ −
assumes a: "QUOTIENT R absf repf"+ −
shows "(if a then b else c) = absf (if a then repf b else repf c)"+ −
using a unfolding QUOTIENT_def by auto+ −
+ −
(* These are the fixed versions, general ones need to be proved. *)+ −
lemma ho_all_prs:+ −
shows "op = ===> op = ===> op = All All"+ −
by auto+ −
+ −
lemma ho_ex_prs: + −
shows "op = ===> op = ===> op = Ex Ex"+ −
by auto+ −
+ −
end+ −
+ −