Quelle W.thy Sprache: Isabelle

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%

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.