Created
May 7, 2020 06:25
-
-
Save hatsugai/d67f7d9d638e84941f7da55927f77926 to your computer and use it in GitHub Desktop.
subsequence
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
theory subseq imports "~~/src/HOL/Hoare/Hoare_Logic" begin | |
definition is_subseq :: "'a list => 'a list => bool" where | |
"is_subseq xs ys == | |
(\<exists>c. | |
(\<forall>i. i + 1 < length ys --> c i < c (i + 1)) | |
\<and> (length ys > 0 \<longrightarrow> c (length ys - 1) < length xs) | |
\<and> (\<forall>i. i < length ys \<longrightarrow> ys ! i = xs ! (c i)))" | |
fun is_subseq2 :: "'a list => 'a list => bool" where | |
"is_subseq2 xs [] = True" | |
| "is_subseq2 [] (y#ys) = False" | |
| "is_subseq2 (x#xs) (y#ys) = | |
(if x=y then is_subseq2 xs ys else is_subseq2 xs (y#ys))" | |
lemma "ALL xs. is_subseq xs ys --> is_subseq2 xs ys" | |
apply(induct_tac ys) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!a list xs. | |
[| ALL xs. is_subseq xs list --> is_subseq2 xs list; | |
is_subseq xs (a # list) |] | |
==> is_subseq2 xs (a # list) | |
*) | |
oops | |
lemma | |
"ALL list. | |
(ALL xs. is_subseq xs list --> is_subseq2 xs list) --> | |
is_subseq xs (a # list) --> | |
is_subseq2 xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
(* | |
1. !!list. | |
[| ALL xs. is_subseq xs list --> is_subseq2 xs list; | |
is_subseq [] (a # list) |] | |
==> False | |
*) | |
oops | |
lemma x1 [dest]: "is_subseq [] (a # list) ==> False" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
done | |
lemma | |
"ALL list. | |
(ALL xs. is_subseq xs list --> is_subseq2 xs list) --> | |
is_subseq xs (a # list) --> | |
is_subseq2 xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
(* | |
goal (2 subgoals): | |
1. !!list lista. | |
[| ALL lista. | |
(ALL xs. | |
is_subseq xs lista --> | |
is_subseq2 xs lista) --> | |
is_subseq list (a # lista) --> | |
is_subseq2 list (a # lista); | |
ALL xs. is_subseq xs lista --> is_subseq2 xs lista; | |
is_subseq (a # list) (a # lista) |] | |
==> is_subseq2 list lista | |
*) | |
oops | |
lemma x2 [dest]: | |
"is_subseq (a # lista) (a # list) ==> is_subseq lista list" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!c. [| ALL i<length list. c i < c (Suc i); | |
c (length list) < Suc (length lista); | |
ALL i<Suc (length list). | |
(a # list) ! i = (a # lista) ! c i |] | |
==> EX c. (ALL i. | |
Suc i < length list --> | |
c i < c (Suc i)) & | |
(list ~= [] --> | |
c (length list - Suc 0) < length lista) & | |
(ALL i<length list. | |
list ! i = lista ! c i) | |
*) | |
apply(rule_tac x="%i. (c (i + 1)) - 1" in exI) | |
apply(auto) | |
apply (metis Suc_lessD diff_less_mono gr_implies_not0 less_Suc0 not_less) | |
apply (metis (erased, hide_lams) Suc_lessD Suc_pred diff_Suc_less gr_implies_not0 length_0_conv less_antisym not_gr0) | |
by (metis One_nat_def Suc_less_eq not_less0 nth_Cons' nth_Cons_Suc) | |
lemma | |
"ALL list. | |
(ALL xs. is_subseq xs list --> is_subseq2 xs list) --> | |
is_subseq xs (a # list) --> | |
is_subseq2 xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!aa list lista. | |
[| ALL lista. | |
(ALL xs. | |
is_subseq xs lista --> | |
is_subseq2 xs lista) --> | |
is_subseq list (a # lista) --> | |
is_subseq2 list (a # lista); | |
aa ~= a; | |
ALL xs. is_subseq xs lista --> is_subseq2 xs lista; | |
is_subseq (aa # list) (a # lista) |] | |
==> is_subseq2 list (a # lista) | |
*) | |
oops | |
lemma x3: | |
"is_subseq (x#xs) (y#ys) ==> | |
x ~= y ==> | |
is_subseq xs (y#ys)" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!c. [| x ~= y; ALL i<length ys. c i < c (Suc i); | |
c (length ys) < Suc (length xs); | |
ALL i<Suc (length ys). | |
(y # ys) ! i = (x # xs) ! c i |] | |
==> EX ca. | |
(ALL i<length ys. ca i < ca (Suc i)) & | |
ca (length ys) < length xs & | |
(ALL i<Suc (length ys). | |
(x # xs) ! c i = xs ! ca i) | |
*) | |
apply(rule_tac x="%i. (c i) - 1" in exI) | |
apply(auto) | |
apply (metis Suc_lessD diff_less_mono less_Suc_eq_0_disj not_less not_less0 nth_Cons' old.nat.exhaust) | |
apply (metis Suc_pred diff_Suc_less length_greater_0_conv less_antisym less_imp_diff_less list.size(3) not_less0 nth_Cons') | |
by (metis One_nat_def less_Suc_eq_0_disj not_less0 nth_Cons') | |
lemma x0 [rule_format]: | |
"ALL list. | |
(ALL xs. is_subseq xs list --> is_subseq2 xs list) --> | |
is_subseq xs (a # list) --> | |
is_subseq2 xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac list) | |
apply(auto) | |
apply(drule x3) | |
apply(assumption) | |
apply(clarsimp) | |
apply(rotate_tac -2) | |
apply(drule_tac x="listb" in spec) | |
apply(rotate_tac -1) | |
apply(drule mp) | |
apply(drule x3) | |
apply(assumption) | |
apply(drule x2) | |
apply(assumption) | |
apply(assumption) | |
apply(drule_tac x="lista" in spec) | |
apply(drule mp) | |
apply(assumption) | |
apply(drule mp) | |
apply(drule x3) | |
apply(assumption) | |
apply(assumption) | |
apply(assumption) | |
done | |
lemma subseq1 [rule_format]: | |
"ALL xs. is_subseq xs ys --> is_subseq2 xs ys" | |
apply(induct_tac ys) | |
apply(auto) | |
apply(rule x0) | |
apply metis | |
apply(assumption) | |
done | |
lemma "ALL xs. is_subseq2 xs ys --> is_subseq xs ys" | |
apply(induct_tac ys) | |
apply(auto) | |
(* | |
goal (2 subgoals): | |
1. !!xs. is_subseq xs [] | |
*) | |
oops | |
lemma x4 [simp]: "is_subseq xs []" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
done | |
lemma "ALL xs. is_subseq2 xs ys --> is_subseq xs ys" | |
apply(induct_tac ys) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!a list xs. | |
[| ALL xs. is_subseq2 xs list --> is_subseq xs list; | |
is_subseq2 xs (a # list) |] | |
==> is_subseq xs (a # list) | |
*) | |
oops | |
lemma | |
"ALL list. | |
(ALL xs. is_subseq2 xs list --> is_subseq xs list) --> | |
is_subseq2 xs (a # list) --> | |
is_subseq xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
(* | |
goal (2 subgoals): | |
1. !!list lista. | |
[| ALL lista. | |
(ALL xs. | |
is_subseq2 xs lista --> | |
is_subseq xs lista) --> | |
is_subseq2 list (a # lista) --> | |
is_subseq list (a # lista); | |
ALL xs. is_subseq2 xs lista --> is_subseq xs lista; | |
is_subseq2 list lista |] | |
==> is_subseq (a # list) (a # lista) | |
*) | |
oops | |
lemma | |
"is_subseq lista list ==> is_subseq (a # lista) (a # list)" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!c. [| ALL i. Suc i < length list --> c i < c (Suc i); | |
ALL i<length list. list ! i = lista ! c i; | |
c (length list - Suc 0) < length lista |] | |
==> EX c. (ALL i<length list. c i < c (Suc i)) & | |
c (length list) < Suc (length lista) & | |
(ALL i<Suc (length list). | |
(a # list) ! i = (a # lista) ! c i) | |
*) | |
apply(rule_tac x="%i. (c (i - 1)) + 1" in exI) | |
apply(auto) | |
(* | |
goal (2 subgoals): | |
1. !!c i. | |
[| ALL i. Suc i < length list --> c i < c (Suc i); | |
ALL i<length list. list ! i = lista ! c i; | |
c (length list - Suc 0) < length lista; | |
i < length list |] | |
==> c (i - Suc 0) < c i | |
*) | |
oops | |
lemma x5: | |
"is_subseq lista list ==> is_subseq (a # lista) (a # list)" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!c. [| ALL i. Suc i < length list --> c i < c (Suc i); | |
ALL i<length list. list ! i = lista ! c i; | |
c (length list - Suc 0) < length lista |] | |
==> EX c. (ALL i<length list. c i < c (Suc i)) & | |
c (length list) < Suc (length lista) & | |
(ALL i<Suc (length list). | |
(a # list) ! i = (a # lista) ! c i) | |
*) | |
apply(rule_tac x="%i. (if i=0 then 0 else (c (i - 1)) + 1)" in exI) | |
apply(auto) | |
by (metis Suc_pred) | |
lemma | |
"ALL list. | |
(ALL xs. is_subseq2 xs list --> is_subseq xs list) --> | |
is_subseq2 xs (a # list) --> | |
is_subseq xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(rule x5) | |
apply metis | |
(* | |
goal (1 subgoal): | |
1. !!aa list lista. | |
[| ALL lista. | |
(ALL xs. | |
is_subseq2 xs lista --> | |
is_subseq xs lista) --> | |
is_subseq2 list (a # lista) --> | |
is_subseq list (a # lista); | |
aa ~= a; | |
ALL xs. is_subseq2 xs lista --> is_subseq xs lista; | |
is_subseq2 list (a # lista) |] | |
==> is_subseq (aa # list) (a # lista) | |
*) | |
oops | |
lemma x7: | |
"is_subseq list (a # lista) ==> | |
aa ~= a ==> | |
is_subseq (aa # list) (a # lista)" | |
apply(unfold is_subseq_def) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!c. [| aa ~= a; ALL i<length lista. c i < c (Suc i); | |
c (length lista) < length list; | |
ALL i<Suc (length lista). | |
(a # lista) ! i = list ! c i |] | |
==> EX ca. | |
(ALL i<length lista. ca i < ca (Suc i)) & | |
ca (length lista) < Suc (length list) & | |
(ALL i<Suc (length lista). | |
list ! c i = (aa # list) ! ca i) | |
*) | |
apply(rule_tac x="%i. (c i) + 1" in exI) | |
apply(auto) | |
done | |
lemma x6: | |
"ALL list. | |
(ALL xs. is_subseq2 xs list --> is_subseq xs list) --> | |
is_subseq2 xs (a # list) --> | |
is_subseq xs (a # list)" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(rule x5) | |
apply metis | |
apply(drule_tac x="lista" in spec) | |
apply(drule mp) | |
apply(assumption) | |
apply(drule mp) | |
apply(assumption) | |
apply(erule x7) | |
apply(assumption) | |
done | |
lemma subseq2 [rule_format]: | |
"ALL xs. is_subseq2 xs ys --> is_subseq xs ys" | |
apply(induct_tac ys) | |
apply(auto) | |
apply(rule x6[rule_format]) | |
apply(auto) | |
done | |
theorem subseq: | |
"is_subseq2 xs ys = is_subseq xs ys" | |
by (metis subseq1 subseq2) | |
(************************************************) | |
lemma | |
"VARS i j | |
{True} | |
i := 0; | |
j := 0; | |
WHILE i < length xs & j < length ys | |
INV { | |
i <= length xs & j <= length ys | |
& is_subseq2 (take i xs) (take j ys) | |
} | |
DO | |
IF xs!i = ys!j THEN | |
i := i + 1; j := j + 1 | |
ELSE | |
i := i + 1 | |
FI | |
OD | |
{(j = length ys) = is_subseq2 xs ys}" | |
apply(vcg) | |
apply(auto) | |
(* | |
goal (4 subgoals): | |
1. !!i j. | |
[| is_subseq2 (take i xs) (take j ys); i < length xs; | |
j < length ys; xs ! i = ys ! j |] | |
==> is_subseq2 (take (Suc i) xs) (take (Suc j) ys) | |
*) | |
oops | |
lemma take_0 [rule_format]: | |
"ALL n. n < length xs --> take (Suc n) xs = take n xs @ [xs!n]" | |
apply(induct_tac xs) | |
apply(auto) | |
by (metis length_Cons take_Suc_Cons take_Suc_conv_app_nth) | |
lemma | |
"VARS i j | |
{True} | |
i := 0; | |
j := 0; | |
WHILE i < length xs & j < length ys | |
INV { | |
i <= length xs & j <= length ys | |
& is_subseq2 (take i xs) (take j ys) | |
} | |
DO | |
IF xs!i = ys!j THEN | |
i := i + 1; j := j + 1 | |
ELSE | |
i := i + 1 | |
FI | |
OD | |
{(j = length ys) = is_subseq2 xs ys}" | |
apply(vcg) | |
apply(auto) | |
apply(subst take_0) | |
apply(assumption) | |
apply(subst take_0) | |
apply(assumption) | |
(* | |
goal (4 subgoals): | |
1. !!i j. | |
[| is_subseq2 (take i xs) (take j ys); i < length xs; | |
j < length ys; xs ! i = ys ! j |] | |
==> is_subseq2 (take i xs @ [xs ! i]) | |
(take j ys @ [ys ! j]) | |
*) | |
oops | |
lemma | |
"ALL ys us vs. | |
is_subseq2 xs ys --> | |
is_subseq2 us vs --> | |
is_subseq2 (xs @ us) (ys @ vs)" | |
apply(induct_tac xs) | |
apply(auto) | |
(* | |
goal (2 subgoals): | |
1. !!ys us vs. | |
[| is_subseq2 [] ys; is_subseq2 us vs |] | |
==> is_subseq2 us (ys @ vs) | |
*) | |
apply(case_tac ys) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!a list ys us vs. | |
[| ALL ys. | |
is_subseq2 list ys --> | |
(ALL us vs. | |
is_subseq2 us vs --> | |
is_subseq2 (list @ us) (ys @ vs)); | |
is_subseq2 (a # list) ys; is_subseq2 us vs |] | |
==> is_subseq2 (a # list @ us) (ys @ vs) | |
*) | |
oops | |
lemma | |
"ALL list us vs. | |
(ALL ys. | |
is_subseq2 list ys --> | |
(ALL us vs. | |
is_subseq2 us vs --> | |
is_subseq2 (list @ us) (ys @ vs))) --> | |
is_subseq2 (a # list) ys --> | |
is_subseq2 us vs --> | |
is_subseq2 (a # list @ us) (ys @ vs)" | |
apply(induct_tac ys) | |
apply(auto) | |
(* | |
goal (1 subgoal): | |
1. !!list us vs. | |
[| ALL ys. | |
is_subseq2 list ys --> | |
(ALL us vs. | |
is_subseq2 us vs --> | |
is_subseq2 (list @ us) (ys @ vs)); | |
is_subseq2 us vs |] | |
==> is_subseq2 (a # list @ us) vs | |
*) | |
oops | |
lemma | |
"ALL xs ys. is_subseq2 xs ys --> is_subseq2 (zs @ xs) ys" | |
apply(induct_tac zs) | |
apply(auto) | |
apply(drule_tac x="xs" in spec) | |
apply(drule_tac x="ys" in spec) | |
apply(drule mp) | |
apply(assumption) | |
(* | |
goal (1 subgoal): | |
1. !!a list xs ys. | |
[| is_subseq2 xs ys; is_subseq2 (list @ xs) ys |] | |
==> is_subseq2 (a # list @ xs) ys | |
*) | |
oops | |
lemma | |
"ALL x ys. is_subseq2 xs ys --> is_subseq2 (x#xs) ys" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac ys) | |
apply(auto) | |
(* | |
2nd induction is needed | |
goal (1 subgoal): | |
1. !!a list x ys. | |
[| ALL x ys. | |
is_subseq2 list ys --> is_subseq2 (x # list) ys; | |
is_subseq2 (a # list) ys |] | |
==> is_subseq2 (x # a # list) ys | |
*) | |
oops | |
lemma x12 [rule_format]: | |
"ALL list a x. | |
(ALL x ys. | |
is_subseq2 list ys --> is_subseq2 (x # list) ys) --> | |
is_subseq2 (a # list) ys --> | |
is_subseq2 (x # a # list) ys" | |
apply(induct_tac ys) | |
apply(auto) | |
by (metis is_subseq2.simps(3)) | |
lemma x11 [rule_format]: | |
"ALL x ys. is_subseq2 xs ys --> is_subseq2 (x#xs) ys" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac ys) | |
apply(auto) | |
apply(rule x12) | |
apply(auto) | |
done | |
lemma x10 [rule_format]: | |
"ALL xs ys. is_subseq2 xs ys --> is_subseq2 (zs @ xs) ys" | |
apply(induct_tac zs) | |
apply(auto) | |
apply(drule_tac x="xs" in spec) | |
apply(drule_tac x="ys" in spec) | |
apply(drule mp) | |
apply(assumption) | |
apply(rule x11) | |
apply(assumption) | |
done | |
lemma x9 [rule_format]: | |
"ALL list us vs. | |
(ALL ys. | |
is_subseq2 list ys --> | |
(ALL us vs. | |
is_subseq2 us vs --> | |
is_subseq2 (list @ us) (ys @ vs))) --> | |
is_subseq2 (a # list) ys --> | |
is_subseq2 us vs --> | |
is_subseq2 (a # list @ us) (ys @ vs)" | |
apply(induct_tac ys) | |
apply(auto) | |
apply(drule_tac zs="a#list" in x10) | |
apply(auto) | |
done | |
lemma subseq_app [rule_format]: | |
"ALL ys us vs. | |
is_subseq2 xs ys --> | |
is_subseq2 us vs --> | |
is_subseq2 (xs @ us) (ys @ vs)" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac ys) | |
apply(auto) | |
apply(rule x9) | |
apply(auto) | |
done | |
lemma | |
"VARS i j | |
{True} | |
i := 0; | |
j := 0; | |
WHILE i < length xs & j < length ys | |
INV { | |
i <= length xs & j <= length ys | |
& is_subseq2 (take i xs) (take j ys) | |
} | |
DO | |
IF xs!i = ys!j THEN | |
i := i + 1; j := j + 1 | |
ELSE | |
i := i + 1 | |
FI | |
OD | |
{(j = length ys) = is_subseq2 xs ys}" | |
apply(vcg) | |
apply(auto) | |
apply(subst take_0) | |
apply(assumption) | |
apply(subst take_0) | |
apply(assumption) | |
apply(rule subseq_app) | |
apply(auto) | |
apply(subst take_0) | |
apply(auto) | |
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app) | |
(* | |
goal (2 subgoals): | |
1. !!j. [| j <= length ys; is_subseq2 xs (take j ys); | |
is_subseq2 xs ys |] | |
==> j = length ys | |
2. !!i. [| i <= length xs; is_subseq2 (take i xs) ys |] | |
==> is_subseq2 xs ys | |
*) | |
oops | |
lemma | |
"ALL zs ys. is_subseq2 xs ys --> is_subseq2 (xs @ zs) ys" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac ys) | |
apply(auto) | |
(* 2nd induction | |
goal (1 subgoal): | |
1. !!a list zs ys. | |
[| ALL zs ys. | |
is_subseq2 list ys --> | |
is_subseq2 (list @ zs) ys; | |
is_subseq2 (a # list) ys |] | |
==> is_subseq2 (a # list @ zs) ys | |
*) | |
oops | |
lemma x14 [rule_format]: | |
"ALL list a ys. | |
(ALL zs ys. | |
is_subseq2 list ys --> is_subseq2 (list @ zs) ys) --> | |
is_subseq2 (a # list) ys --> | |
is_subseq2 (a # list @ zs) ys" | |
apply(induct_tac zs) | |
apply(auto) | |
by (metis append_Cons append_Nil2 is_subseq2.simps(1) subseq_app) | |
lemma x13 [rule_format]: | |
"ALL zs ys. is_subseq2 xs ys --> is_subseq2 (xs @ zs) ys" | |
apply(induct_tac xs) | |
apply(auto) | |
apply(case_tac ys) | |
apply(auto) | |
apply(rule x14) | |
apply(auto) | |
done | |
lemma | |
"VARS i j | |
{True} | |
i := 0; | |
j := 0; | |
WHILE i < length xs & j < length ys | |
INV { | |
i <= length xs & j <= length ys | |
& is_subseq2 (take i xs) (take j ys) | |
} | |
DO | |
IF xs!i = ys!j THEN | |
i := i + 1; j := j + 1 | |
ELSE | |
i := i + 1 | |
FI | |
OD | |
{(j = length ys) = is_subseq2 xs ys}" | |
apply(vcg) | |
apply(auto) | |
apply(subst take_0) | |
apply(assumption) | |
apply(subst take_0) | |
apply(assumption) | |
apply(rule subseq_app) | |
apply(auto) | |
apply(subst take_0) | |
apply(auto) | |
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app) | |
defer | |
apply (metis append_take_drop_id x13) | |
oops | |
lemma | |
"VARS i j | |
{True} | |
i := 0; | |
j := 0; | |
WHILE i < length xs & j < length ys | |
INV { | |
i <= length xs & j <= length ys | |
& is_subseq2 (take i xs) (take j ys) | |
& (is_subseq2 xs ys --> is_subseq2 (drop i xs) (drop j ys)) | |
} | |
DO | |
IF xs!i = ys!j THEN | |
i := i + 1; j := j + 1 | |
ELSE | |
i := i + 1 | |
FI | |
OD | |
{(j = length ys) = is_subseq2 xs ys}" | |
apply(vcg) | |
apply(auto) | |
apply(subst take_0) | |
apply(assumption) | |
apply(subst take_0) | |
apply(assumption) | |
apply(rule subseq_app) | |
apply(auto) | |
apply(subst take_0) | |
apply(auto) | |
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app) | |
apply(subst take_0) | |
apply(assumption) | |
apply(subst take_0) | |
apply(assumption) | |
apply(rule subseq_app) | |
apply(auto) | |
apply (metis Cons_nth_drop_Suc is_subseq2.simps(3)) | |
apply (metis take_hd_drop x13) | |
apply (metis Cons_nth_drop_Suc is_subseq2.simps(3)) | |
apply (metis append_take_drop_id x13) | |
apply (meson antisym_conv drop_eq_Nil is_subseq2.elims(2) list.distinct(1)) | |
by (metis append_take_drop_id x13) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment