Quelle W.thy Sprache: unbekannt

theory W
imports "HOL-Nominal.Nominal"
begin

text \<open>Example for strong induction rules avoiding sets of atoms.\<close>

atom_decl tvar var

abbreviation
  "difference_list" :: "'a list \ 'a list \ 'a list" (\_ - _\ [60,60] 60)
where
  "xs - ys \ [x \ xs. x\set ys]"

lemma difference_eqvt_tvar[eqvt]:
  fixes pi::"tvar prm"
    and   Xs Ys::"tvar list"
  shows "pi\(Xs - Ys) = (pi\Xs) - (pi\Ys)"
  by (induct Xs) (simp_all add: eqvts)

lemma difference_fresh [simp]:
  fixes X::"tvar"
    and   Xs Ys::"tvar list"
  shows "X\(Xs - Ys) \ X\Xs \ X\set Ys"
  by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)

lemma difference_supset:
  fixes xs::"'a list"
  and   ys::"'a list"
  and   zs::"'a list"
  assumes asm: "set xs \ set ys"
  shows "xs - ys = []"
using asm
by (induct xs) (auto)

nominal_datatype ty =
    TVar "tvar"
  | Fun "ty" "ty" (\<open>_\<rightarrow>_\<close> [100,100] 100)

nominal_datatype tyS =
    Ty  "ty"
  | ALL "\tvar\tyS" (\\[_]._\ [100,100] 100)

nominal_datatype trm =
    Var "var"
  | App "trm" "trm"
  | Lam "\var\trm" (\Lam [_]._\ [100,100] 100)
  | Let "\var\trm" "trm"

abbreviation
  LetBe :: "var \ trm \ trm \ trm" (\Let _ be _ in _\ [100,100,100] 100)
where
"Let x be t1 in t2 \ trm.Let x t2 t1"

type_synonym
  Ctxt  = "(var\tyS) list"

text \<open>free type variables\<close>

consts ftv :: "'a \ tvar list"

overloading
  ftv_prod \<equiv> "ftv :: ('a \<times> 'b) \<Rightarrow> tvar list"
  ftv_tvar \<equiv> "ftv :: tvar \<Rightarrow> tvar list"
  ftv_var  \<equiv> "ftv :: var \<Rightarrow> tvar list"
  ftv_list \<equiv> "ftv :: 'a list \<Rightarrow> tvar list"
  ftv_ty   \<equiv> "ftv :: ty \<Rightarrow> tvar list"
begin

primrec
  ftv_prod
where
"ftv_prod (x, y) = (ftv x) @ (ftv y)"

definition
  ftv_tvar :: "tvar \ tvar list"
where
[simp]: "ftv_tvar X \ [(X::tvar)]"

definition
  ftv_var :: "var \ tvar list"
where
[simp]: "ftv_var x \ []"

primrec
  ftv_list
where
  "ftv_list [] = []"
| "ftv_list (x#xs) = (ftv x)@(ftv_list xs)"

nominal_primrec
  ftv_ty :: "ty \ tvar list"
where
  "ftv_ty (TVar X) = [X]"
| "ftv_ty (T1 \T2) = (ftv_ty T1) @ (ftv_ty T2)"
by (rule TrueI)+

end

lemma ftv_ty_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   T::"ty"
  shows "pi\(ftv T) = ftv (pi\T)"
by (nominal_induct T rule: ty.strong_induct)
   (perm_simp add: append_eqvt)+

overloading
  ftv_tyS  \<equiv> "ftv :: tyS \<Rightarrow> tvar list"
begin

nominal_primrec
  ftv_tyS :: "tyS \ tvar list"
where
  "ftv_tyS (Ty T) = ((ftv (T::ty))::tvar list)"
| "ftv_tyS (\[X].S) = (ftv_tyS S) - [X]"
apply(finite_guess add: ftv_ty_eqvt fs_tvar1 | rule TrueI)+
  apply (metis difference_fresh list.set_intros(1))
apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
done

end

lemma ftv_tyS_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   S::"tyS"
  shows "pi\(ftv S) = ftv (pi\S)"
proof (nominal_induct S rule: tyS.strong_induct)
  case (Ty ty)
  then show ?case
    by (simp add: ftv_ty_eqvt)
next
  case (ALL tvar tyS)
  then show ?case
    by (metis difference_eqvt_tvar ftv_ty.simps(1) ftv_tyS.simps(2) ftv_ty_eqvt ty.perm(3) tyS.perm(4))
qed

lemma ftv_Ctxt_eqvt[eqvt]:
  fixes pi::"tvar prm"
    and   \<Gamma>::"Ctxt"
  shows "pi\(ftv \) = ftv (pi\\)"
  by (induct \<Gamma>) (auto simp add: eqvts)

text \<open>Valid\<close>
inductive
  valid :: "Ctxt \ bool"
where
  V_Nil[intro]:  "valid []"
| V_Cons[intro]: "\valid \;x\\\\ valid ((x,S)#\)"

equivariance valid

text \<open>General\<close>
primrec gen :: "ty \ tvar list \ tyS" where
  "gen T [] = Ty T"
| "gen T (X#Xs) = \[X].(gen T Xs)"

lemma gen_eqvt[eqvt]:
  fixes pi::"tvar prm"
  shows "pi\(gen T Xs) = gen (pi\T) (pi\Xs)"
  by (induct Xs) (simp_all add: eqvts)

abbreviation
  close :: "Ctxt \ ty \ tyS"
where
  "close \ T \ gen T ((ftv T) - (ftv \))"

lemma close_eqvt[eqvt]:
  fixes pi::"tvar prm"
  shows "pi\(close \ T) = close (pi\\) (pi\T)"
  by (simp_all only: eqvts)

text \<open>Substitution\<close>

type_synonym Subst = "(tvar\ty) list"

consts
  psubst :: "Subst \ 'a \ 'a" (\_<_>\ [100,60] 120)

abbreviation
  subst :: "'a \ tvar \ ty \ 'a" (\_[_::=_]\ [100,100,100] 100)
where
  "smth[X::=T] \ ([(X,T)])"

fun lookup :: "Subst \ tvar \ ty"
where
  "lookup [] X = TVar X"
| "lookup ((Y,T)#\) X = (if X=Y then T else lookup \ X)"

lemma lookup_eqvt[eqvt]:
  fixes pi::"tvar prm"
  shows "pi\(lookup \ X) = lookup (pi\\) (pi\X)"
  by (induct \<theta>) (auto simp add: eqvts)

lemma lookup_fresh:
  fixes X::"tvar"
  assumes a: "X\\"
  shows "lookup \ X = TVar X"
  using a
  by (induct \<theta>)
    (auto simp add: fresh_list_cons fresh_prod fresh_atm)

overloading
  psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty"
begin

nominal_primrec
  psubst_ty
where
  "\ = lookup \ X"
| "\1 \ T\<^sub>2> = (\1>) \ (\2>)"
by (rule TrueI)+

end

lemma psubst_ty_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   \<theta>::"Subst"
  and   T::"ty"
  shows "pi\(\) = (pi\\)<(pi\T)>"
by (induct T rule: ty.induct) (simp_all add: eqvts)

overloading
  psubst_tyS \<equiv> "psubst :: Subst \<Rightarrow> tyS \<Rightarrow> tyS"
begin

nominal_primrec
  psubst_tyS :: "Subst \ tyS \ tyS"
where
  "\<(Ty T)> = Ty (\)"
| "X\\ \ \<(\[X].S)> = \[X].(\)"
apply(finite_guess add: psubst_ty_eqvt fs_tvar1 | simp add: abs_fresh)+
apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+
done

end

overloading
  psubst_Ctxt \<equiv> "psubst :: Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt"
begin

fun
  psubst_Ctxt :: "Subst \ Ctxt \ Ctxt"
where
  "psubst_Ctxt \ [] = []"
| "psubst_Ctxt \ ((x,S)#\) = (x,\~~)#(psubst_Ctxt \ \)"~~

end

lemma fresh_lookup:
  fixes X::"tvar"
  and   \<theta>::"Subst"
  and   Y::"tvar"
  assumes asms: "X\Y" "X\\"
  shows "X\(lookup \ Y)"
  using asms
  by (induct \<theta>)
     (auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma fresh_psubst_ty:
  fixes X::"tvar"
  and   \<theta>::"Subst"
  and   T::"ty"
  assumes asms: "X\\" "X\T"
  shows "X\\"
  using asms
  by (nominal_induct T rule: ty.strong_induct)
     (auto simp add: fresh_list_append fresh_list_cons fresh_prod fresh_lookup)

lemma fresh_psubst_tyS:
  fixes X::"tvar"
  and   \<theta>::"Subst"
  and   S::"tyS"
  assumes asms: "X\\" "X\S"
  shows "X\\"
  using asms
  by (nominal_induct S avoiding: \<theta>  X rule: tyS.strong_induct)
     (auto simp add: fresh_psubst_ty abs_fresh)

lemma fresh_psubst_Ctxt:
  fixes X::"tvar"
  and   \<theta>::"Subst"
  and   \<Gamma>::"Ctxt"
  assumes asms: "X\\" "X\\"
  shows "X\\<\>"
using asms
by (induct \<Gamma>)
   (auto simp add: fresh_psubst_tyS fresh_list_cons)

lemma subst_freshfact2_ty:
  fixes   X::"tvar"
  and     Y::"tvar"
  and     T::"ty"
  assumes asms: "X\S"
  shows "X\T[X::=S]"
  using asms
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_atm)

text \<open>instance of a type scheme\<close>
inductive
  inst :: "ty \ tyS \ bool"(\_ \ _\ [50,51] 50)
where
  I_Ty[intro]:  "T \ (Ty T)"
| I_All[intro]: "\X\T'; T \ S\ \ T[X::=T'] \ \[X].S"

equivariance inst[tvar]

nominal_inductive inst
  by (simp_all add: abs_fresh subst_freshfact2_ty)

lemma subst_forget_ty:
  fixes T::"ty"
  and   X::"tvar"
  assumes a: "X\T"
  shows "T[X::=S] = T"
  using a
  by  (nominal_induct T rule: ty.strong_induct)
      (auto simp add: fresh_atm)

lemma psubst_ty_lemma:
  fixes \<theta>::"Subst"
  and   X::"tvar"
  and   T'::"ty"
  and   T::"ty"
  assumes a: "X\\"
  shows "\ = (\)[X::=\]"
using a
proof (nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct)
  case (TVar tvar)
  then show ?case
    by (simp add: fresh_atm(1) fresh_lookup lookup_fresh subst_forget_ty)
qed auto

lemma general_preserved:
  fixes \<theta>::"Subst"
  assumes a: "T \ S"
  shows "\ \ \"
  using a
proof (nominal_induct T S avoiding: \<theta> rule: inst.strong_induct)
  case (I_Ty T)
  then show ?case
    by (simp add: inst.I_Ty)
next
  case (I_All X T' T S)
  then show ?case
    by (simp add: fresh_psubst_ty inst.I_All psubst_ty_lemma)
qed

text\<open>typing judgements\<close>
inductive
  typing :: "Ctxt \ trm \ ty \ bool" (\ _ \ _ : _ \ [60,60,60] 60)
where
  T_VAR[intro]: "\valid \; (x,S)\set \; T \ S\\ \ \ Var x : T"
| T_APP[intro]: "\\ \ t\<^sub>1 : T\<^sub>1\T\<^sub>2; \ \ t\<^sub>2 : T\<^sub>1\\ \ \ App t\<^sub>1 t\<^sub>2 : T\<^sub>2"
| T_LAM[intro]: "\x\\;((x,Ty T\<^sub>1)#\) \ t : T\<^sub>2\ \ \ \ Lam [x].t : T\<^sub>1\T\<^sub>2"
| T_LET[intro]: "\x\\; \ \ t\<^sub>1 : T\<^sub>1; ((x,close \ T\<^sub>1)#\) \ t\<^sub>2 : T\<^sub>2; set (ftv T\<^sub>1 - ftv \) \* T\<^sub>2\
                 \<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2"

equivariance typing[tvar]

lemma fresh_tvar_trm:
  fixes X::"tvar"
  and   t::"trm"
  shows "X\t"
by (nominal_induct t rule: trm.strong_induct)
   (simp_all add: fresh_atm abs_fresh)

lemma ftv_ty:
  fixes T::"ty"
  shows "supp T = set (ftv T)"
by (nominal_induct T rule: ty.strong_induct)
   (simp_all add: ty.supp supp_atm)

lemma ftv_tyS:
  fixes S::"tyS"
  shows "supp S = set (ftv S)"
by (nominal_induct S rule: tyS.strong_induct)
   (auto simp add: tyS.supp abs_supp ftv_ty)

lemma ftv_Ctxt:
  fixes \<Gamma>::"Ctxt"
  shows "supp \ = set (ftv \)"
proof (induct \<Gamma>)
  case Nil
  then show ?case
    by (simp add: supp_list_nil)
next
  case (Cons c \<Gamma>)
  show ?case
  proof (cases c)
    case (Pair a b)
    with Cons show ?thesis
      by (simp add: ftv_tyS supp_atm(3) supp_list_cons supp_prod)
  qed
qed

lemma ftv_tvars:
  fixes Tvs::"tvar list"
  shows "supp Tvs = set Tvs"
  by (induct Tvs) (simp_all add: supp_list_nil supp_list_cons supp_atm)

lemma difference_supp:
  fixes xs ys::"tvar list"
  shows "((supp (xs - ys))::tvar set) = supp xs - supp ys"
  by (induct xs) (auto simp add: supp_list_nil supp_list_cons ftv_tvars)

lemma set_supp_eq:
  fixes xs::"tvar list"
  shows "set xs = supp xs"
  by (induct xs) (simp_all add: supp_list_nil supp_list_cons supp_atm)

nominal_inductive2 typing
  avoids T_LET: "set (ftv T\<^sub>1 - ftv \)"
     apply (simp_all add: fresh_star_def fresh_def ftv_Ctxt fresh_tvar_trm)
  by (meson fresh_def fresh_tvar_trm)

lemma perm_fresh_fresh_aux:
  "\(x,y)\set (pi::tvar prm). x \ z \ y \ z \ pi \ (z::'a::pt_tvar) = z"
proof (induct pi rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc x xs)
  then show ?case
    unfolding split_paired_all pt_tvar2
    using perm_fresh_fresh(1) by fastforce
qed

lemma freshs_mem:
  fixes S::"tvar set"
  assumes "x \ S"
    and     "S \* z"
  shows  "x \ z"
  using assms by (simp add: fresh_star_def)

lemma fresh_gen_set:
  fixes X::"tvar"
  and   Xs::"tvar list"
  assumes "X\set Xs"
  shows "X\gen T Xs"
  using assms by (induct Xs) (auto simp: abs_fresh)

lemma close_fresh:
  fixes \<Gamma>::"Ctxt"
  shows "\(X::tvar)\set ((ftv T) - (ftv \)). X\(close \ T)"
  by (meson fresh_gen_set)

lemma gen_supp:
  shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs"
by (induct Xs)
   (auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm)

lemma minus_Int_eq:
  shows "T - (T - U) = T \ U"
  by blast

lemma close_supp:
  shows "supp (close \ T) = set (ftv T) \ set (ftv \)"
  using difference_supp ftv_ty gen_supp set_supp_eq by auto

lemma better_T_LET:
  assumes x: "x\\"
  and t1: "\ \ t\<^sub>1 : T\<^sub>1"
  and t2: "((x,close \ T\<^sub>1)#\) \ t\<^sub>2 : T\<^sub>2"
  shows "\ \ Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2"
proof -
  have fin: "finite (set (ftv T\<^sub>1 - ftv \))" by simp
  obtain pi where pi1: "(pi \ set (ftv T\<^sub>1 - ftv \)) \* (T\<^sub>2, \)"
    and pi2: "set pi \ set (ftv T\<^sub>1 - ftv \) \ (pi \ set (ftv T\<^sub>1 - ftv \))"
    by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^sub>2, \)"])
  from pi1 have pi1': "(pi \ set (ftv T\<^sub>1 - ftv \)) \* \"
    by (simp add: fresh_star_prod)
  have Gamma_fresh: "\(x,y)\set pi. x \ \ \ y \ \"
    using freshs_mem [OF _ pi1'] subsetD [OF pi2] ftv_Ctxt fresh_def by fastforce
  have "\x y. \x \ set (ftv T\<^sub>1 - ftv \); y \ pi \ set (ftv T\<^sub>1 - ftv \)\
              \<Longrightarrow> x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
    using pi1' fresh_def fresh_gen_set freshs_mem ftv_Ctxt ftv_ty gen_supp
    by (metis (lifting) DiffE mem_Collect_eq set_filter)
  then have close_fresh': "\(x, y)\set pi. x \ close \ T\<^sub>1 \ y \ close \ T\<^sub>1"
    using pi2 by auto
  note x
  moreover from Gamma_fresh perm_boolI [OF t1, of pi]
  have "\ \ t\<^sub>1 : pi \ T\<^sub>1"
    by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
  moreover from t2 close_fresh'
  have "(x,(pi \ close \ T\<^sub>1))#\ \ t\<^sub>2 : T\<^sub>2"
    by (simp add: perm_fresh_fresh_aux)
  with Gamma_fresh have "(x,close \ (pi \ T\<^sub>1))#\ \ t\<^sub>2 : T\<^sub>2"
    by (simp add: close_eqvt perm_fresh_fresh_aux)
  moreover from pi1 Gamma_fresh
  have "set (ftv (pi \ T\<^sub>1) - ftv \) \* T\<^sub>2"
    by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux)
  ultimately show ?thesis by (rule T_LET)
qed

lemma ftv_ty_subst:
  fixes T::"ty"
  and   \<theta>::"Subst"
  and   X Y ::"tvar"
  assumes "X \ set (ftv T)"
  and     "Y \ set (ftv (lookup \ X))"
  shows "Y \ set (ftv (\))"
  using assms
  by (nominal_induct T rule: ty.strong_induct) (auto)

lemma ftv_tyS_subst:
  fixes S::"tyS"
  and   \<theta>::"Subst"
  and   X Y::"tvar"
  assumes "X \ set (ftv S)"
  and     "Y \ set (ftv (lookup \ X))"
  shows "Y \ set (ftv (\~~))"~~
  using assms
by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct)
   (auto simp add: ftv_ty_subst fresh_atm)

lemma ftv_Ctxt_subst:
  fixes \<Gamma>::"Ctxt"
  and   \<theta>::"Subst"
assumes "X \ set (ftv \)"
  and   "Y \ set (ftv (lookup \ X))"
  shows "Y \ set (ftv (\<\>))"
  using assms by (induct \<Gamma>) (auto simp add: ftv_tyS_subst)

lemma gen_preserved1:
  assumes "Xs \* \"
  shows "\ = gen (\) Xs"
  using assms by (induct Xs) (auto simp add: fresh_star_def)

lemma gen_preserved2:
  fixes T::"ty"
  and   \<Gamma>::"Ctxt"
  assumes "((ftv T) - (ftv \)) \* \"
  shows "((ftv (\)) - (ftv (\<\>))) = ((ftv T) - (ftv \))"
  using assms
proof(nominal_induct T rule: ty.strong_induct)
  case (TVar tvar)
  then show ?case
    apply(auto simp add: fresh_star_def ftv_Ctxt_subst)
    by (metis filter.simps fresh_def fresh_psubst_Ctxt ftv_Ctxt ftv_ty.simps(1) lookup_fresh)
next
  case (Fun ty1 ty2)
  then show ?case
    by (simp add: fresh_star_list)
qed

lemma close_preserved:
  fixes \<Gamma>::"Ctxt"
  assumes "((ftv T) - (ftv \)) \* \"
  shows "\ T> = close (\<\>) (\)"
  using assms by (simp add: gen_preserved1 gen_preserved2)

lemma var_fresh_for_ty:
  fixes x::"var"
    and   T::"ty"
  shows "x\T"
  by (nominal_induct T rule: ty.strong_induct) (simp_all add: fresh_atm)

lemma var_fresh_for_tyS:
  fixes x::"var" and S::"tyS"
  shows "x\S"
  by (nominal_induct S rule: tyS.strong_induct) (simp_all add: abs_fresh var_fresh_for_ty)

lemma psubst_fresh_Ctxt:
  fixes x::"var" and \<Gamma>::"Ctxt" and \<theta>::"Subst"
  shows "x\\<\> = x\\"
  by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)

lemma psubst_valid:
  fixes \<theta>::Subst
    and   \<Gamma>::Ctxt
  assumes "valid \"
  shows "valid (\<\>)"
  using assms by (induct) (auto simp add: psubst_fresh_Ctxt)

lemma psubst_in:
  fixes \<Gamma>::"Ctxt"
  and   \<theta>::"Subst"
  and   pi::"tvar prm"
  and   S::"tyS"
  assumes a: "(x,S)\set \"
  shows "(x,\~~)\set (\<\>)"~~
  using a by (induct \<Gamma>) (auto simp add: calc_atm)

lemma typing_preserved:
  fixes \<theta>::"Subst"
    and   pi::"tvar prm"
  assumes "\ \ t : T"
  shows "(\<\>) \ t : (\)"
  using assms
proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct)
  case (T_VAR \<Gamma> x S T)
  have a1: "valid \" by fact
  have a2: "(x, S) \ set \" by fact
  have a3: "T \ S" by fact
  have  "valid (\<\>)" using a1 by (simp add: psubst_valid)
  moreover
  have  "(x,\~~)\set (\<\>)" using a2 by (simp add: psubst_in)~~
  moreover
  have "\ \ \~~" using a3 by (simp add: general_preserved)~~
  ultimately show "(\<\>) \ Var x : (\)" by (simp add: typing.T_VAR)
next
  case (T_APP \<Gamma> t1 T1 T2 t2)
  have "\<\> \ t1 : \ T2>" by fact
  then have "\<\> \ t1 : (\) \ (\)" by simp
  moreover
  have "\<\> \ t2 : \" by fact
  ultimately show "\<\> \ App t1 t2 : \" by (simp add: typing.T_APP)
next
  case (T_LAM x \<Gamma> T1 t T2)
  fix pi::"tvar prm" and \<theta>::"Subst"
  have "x\\" by fact
  then have "x\\<\>" by (simp add: psubst_fresh_Ctxt)
  moreover
  have "\<((x, Ty T1)#\)> \ t : \" by fact
  then have "((x, Ty (\))#(\<\>)) \ t : \" by (simp add: calc_atm)
  ultimately show "\<\> \ Lam [x].t : \ T2>" by (simp add: typing.T_LAM)
next
  case (T_LET x \<Gamma> t1 T1 t2 T2)
  have vc: "((ftv T1) - (ftv \)) \* \" by fact
  have "x\\" by fact
   then have a1: "x\\<\>" by (simp add: calc_atm psubst_fresh_Ctxt)
  have a2: "\<\> \ t1 : \" by fact
  have a3: "\<((x, close \ T1)#\)> \ t2 : \" by fact
  from a2 a3 show "\<\> \ Let x be t1 in t2 : \"
    by (simp add: a1 better_T_LET close_preserved vc)
qed

end

quality85%

~~[ Verzeichnis aufwärts0.22unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ]~~