tm: comparison thys2/UF

equal deleted inserted replaced

-:b1b47d28c295
+:28d85e8ff391
 theory UF_Rec
 imports Recs Turing2
 begin
-section {* Coding of Turing Machines and tapes*}
+section {* Coding of Turing Machines and Tapes*}
-text {*
-The purpose of this section is to construct the coding function of Turing
+fun actnum :: "action \<Rightarrow> nat"
-Machine, which is going to be named @{text "code"}. *}
+where
+"actnum W0 = 0"
-text {* Encoding of actions as numbers *}
+| "actnum W1 = 1"
+| "actnum L  = 2"
-fun action_num :: "action \<Rightarrow> nat"
+| "actnum R  = 3"
-where
+| "actnum Nop = 4"
-"action_num W0 = 0"
-| "action_num W1 = 1"
+fun cellnum :: "cell \<Rightarrow> nat" where
-| "action_num L  = 2"
+"cellnum Bk = 0"
-| "action_num R  = 3"
+| "cellnum Oc = 1"
-| "action_num Nop = 4"
+text {* Coding tapes *}
-fun cell_num :: "cell \<Rightarrow> nat" where
-"cell_num Bk = 0"
-| "cell_num Oc = 1"
 fun code_tp :: "cell list \<Rightarrow> nat list"
 where
 "code_tp [] = []"
-| "code_tp (c # tp) = (cell_num c) # code_tp tp"
+| "code_tp (c # tp) = (cellnum c) # code_tp tp"
 fun Code_tp where
 "Code_tp tp = lenc (code_tp tp)"
 lemma code_tp_append [simp]:
 lemma code_tp_length [simp]:
 "length (code_tp tp) = length tp"
 by (induct tp) (simp_all)
 lemma code_tp_nth [simp]:
-"n < length tp \<Longrightarrow> (code_tp tp) ! n = cell_num (tp ! n)"
+"n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
 apply(induct n arbitrary: tp)
 apply(simp_all)
 apply(case_tac [!] tp)
 apply(simp_all)
 done
 lemma code_tp_replicate [simp]:
-"code_tp (c \<up> n) = (cell_num c) \<up> n"
+"code_tp (c \<up> n) = (cellnum c) \<up> n"
 by(induct n) (simp_all)
+text {* Coding Configurations and TMs *}
 fun Code_conf where
 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
 fun code_instr :: "instr \<Rightarrow> nat" where
-"code_instr i = penc (action_num (fst i)) (snd i)"
+"code_instr i = penc (actnum (fst i)) (snd i)"
 fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where
 "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"
 fun code_tprog :: "tprog \<Rightarrow> nat list"
 fun Code_tprog :: "tprog \<Rightarrow> nat"
 where
 "Code_tprog tm = lenc (code_tprog tm)"
-section {* Universal Function in HOL *}
+section {* An Universal Function in HOL *}
 text {* Reading and writing the encoded tape *}
 fun Read where
 "Read tp = ldec tp 0"
 fun Write where
 "Write n tp = penc (Suc n) (pdec2 tp)"
 text {*
 The @{text Newleft} and @{text Newright} functions on page 91 of B book.
-They calculate the new left and right tape (@{text p} and @{text r}) according
+They calculate the new left and right tape (@{text p} and @{text r})
-to an action @{text a}.
+according to an action @{text a}. Adapted to our encoding functions.
 *}
 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "Newleft l r a = (if a = 0 then l else
 "Left cf = ldec cf 1"
 fun Right where
 "Right cf = ldec cf 2"
+text {*
+@{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of
+execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM.
+*}
 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)),
 Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
 Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
-text {*
-@{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
-of TM coded as @{text "m"}.
-*}
 fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "Steps cf p 0  = cf"
 | "Steps cf p (Suc n) = Steps (Step cf p) p n"
 lemma Step_Steps_comm:
 "Step (Steps cf p n) p = Steps (Step cf p) p n"
 by (induct n arbitrary: cf) (simp_all only: Steps.simps)
-text {*
+text {* Decoding tapes back into numbers. *}
-Decoding tapes into binary or stroke numbers.
-*}
 definition Stknum :: "nat \<Rightarrow> nat"
 where
 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)"
-definition
-"right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
-definition
-"left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
-lemma ww:
-"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow>
-(\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
-apply(rule iffI)
-apply(erule exE)+
-apply(simp)
-apply(rule_tac x="k" in exI)
-apply(auto)[1]
-apply(simp add: nth_append)
-apply(simp add: nth_append)
-apply(erule exE)
-apply(rule_tac x="i" in exI)
-apply(rule_tac x="length tp - i" in exI)
-apply(auto)
-apply(rule sym)
-apply(subst append_eq_conv_conj)
-apply(simp)
-apply(rule conjI)
-apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
-by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
-lemma right_std:
-"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
-apply(simp only: ww)
-apply(simp add: right_std_def)
-apply(simp only: list_encode_inverse)
-apply(simp)
-apply(auto)
-apply(rule_tac x="i" in exI)
-apply(simp)
-apply(rule conjI)
-apply (metis Suc_eq_plus1 Suc_neq_Zero cell_num.cases cell_num.simps(1) leD less_trans linorder_neqE_nat)
-apply(auto)
-by (metis One_nat_def cell_num.cases cell_num.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
-lemma left_std:
-"(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
-apply(simp add: left_std_def)
-apply(simp only: list_encode_inverse)
-apply(simp)
-apply(auto)
-apply(rule_tac x="length tp" in exI)
-apply(induct tp)
-apply(simp)
-apply(simp)
-apply(auto)
-apply(case_tac a)
-apply(auto)
-apply(case_tac a)
-apply(auto)
-by (metis Suc_less_eq nth_Cons_Suc)
 lemma Stknum_append:
 "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)"
 apply(simp only: Code_tp.simps)
 apply(simp only: code_tp_append)
 "Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n"
 apply(simp only: Stknum_append)
 apply(simp only: tape_of_nat.simps)
 apply(simp only: Code_tp.simps)
 apply(simp only: code_tp_replicate)
-apply(simp only: cell_num.simps)
+apply(simp only: cellnum.simps)
 apply(simp only: Stknum_up)
 apply(simp)
 done
+section  {* Standard Tapes *}
+definition
+"right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
+definition
+"left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
+lemma ww:
+"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow>
+(\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
+apply(rule iffI)
+apply(erule exE)+
+apply(simp)
+apply(rule_tac x="k" in exI)
+apply(auto)[1]
+apply(simp add: nth_append)
+apply(simp add: nth_append)
+apply(erule exE)
+apply(rule_tac x="i" in exI)
+apply(rule_tac x="length tp - i" in exI)
+apply(auto)
+apply(rule sym)
+apply(subst append_eq_conv_conj)
+apply(simp)
+apply(rule conjI)
+apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
+by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
+lemma right_std:
+"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
+apply(simp only: ww)
+apply(simp add: right_std_def)
+apply(simp only: list_encode_inverse)
+apply(simp)
+apply(auto)
+apply(rule_tac x="i" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat)
+apply(auto)
+by (metis One_nat_def cellnum.cases cellnum.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
+lemma left_std:
+"(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
+apply(simp add: left_std_def)
+apply(simp only: list_encode_inverse)
+apply(simp)
+apply(auto)
+apply(rule_tac x="length tp" in exI)
+apply(induct tp)
+apply(simp)
+apply(simp)
+apply(auto)
+apply(case_tac a)
+apply(auto)
+apply(case_tac a)
+apply(auto)
+by (metis Suc_less_eq nth_Cons_Suc)
+section {* Standard- and Final Configurations, the Universal Function *}
 text {*
 @{text "Std cf"} returns true, if the  configuration  @{text "cf"}
 is a stardard tape.
 *}
 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "Halt m cf = (LEAST k. Stop m cf k)"
-thm Steps.simps
 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
 "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
-section {* The UF can simulate Turing machines *}
+section {* The UF simulates Turing machines *}
 lemma Update_left_simulate:
-shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))"
+shows "Newleft (Code_tp l) (Code_tp r) (actnum a) = Code_tp (fst (update a (l, r)))"
 apply(induct a)
 apply(simp_all)
 apply(case_tac l)
 apply(simp_all)
 apply(case_tac r)
 apply(simp_all)
 done
 lemma Update_right_simulate:
-shows "Newright (Code_tp l) (Code_tp r) (action_num a) = Code_tp (snd (update a (l, r)))"
+shows "Newright (Code_tp l) (Code_tp r) (actnum a) = Code_tp (snd (update a (l, r)))"
 apply(induct a)
 apply(simp_all)
 apply(case_tac r)
 apply(simp_all)
 apply(case_tac r)
 apply(case_tac r)
 apply(simp_all)
 done
 lemma Fetch_state_simulate:
-"tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)"
+"tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cellnum c) = snd (fetch tp st c)"
 apply(induct tp st c rule: fetch.induct)
 apply(simp_all add: list_encode_inverse split: cell.split)
 done
 lemma Fetch_action_simulate:
-"tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
+"tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cellnum c) = actnum (fst (fetch tp st c))"
 apply(induct tp st c rule: fetch.induct)
 apply(simp_all add: list_encode_inverse split: cell.split)
 done
 lemma Read_simulate:
-"Read (Code_tp tp) = cell_num (read tp)"
+"Read (Code_tp tp) = cellnum (read tp)"
 apply(case_tac tp)
 apply(simp_all)
 done
 lemma misc:
 "rec_read = CN rec_ldec [Id 1 0, constn 0]"
 definition
 "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"
-lemma read_lemma [simp]:
-"rec_eval rec_read [x] = Read x"
-by (simp add: rec_read_def)
-lemma write_lemma [simp]:
-"rec_eval rec_write [x, y] = Write x y"
-by (simp add: rec_write_def)
 definition
 "rec_newleft =
 (let cond0 = CN rec_eq [Id 3 2, constn 0] in
 let cond1 = CN rec_eq [Id 3 2, constn 1] in
 let cond2 = CN rec_eq [Id 3 2, constn 2] in
 CN rec_if [cond0, CN rec_write [constn 0, Id 3 1],
 CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],
 CN rec_if [cond2, case2,
 CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"
-lemma newleft_lemma [simp]:
-"rec_eval rec_newleft [p, r, a] = Newleft p r a"
-by (simp add: rec_newleft_def Let_def)
-lemma newright_lemma [simp]:
-"rec_eval rec_newright [p, r, a] = Newright p r a"
-by (simp add: rec_newright_def Let_def)
 definition
 "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])
 (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"
-lemma act_lemma [simp]:
-"rec_eval rec_actn [n, c] = Actn n c"
-apply(simp add: rec_actn_def)
-apply(case_tac c)
-apply(simp_all)
-done
 definition
 "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in
 let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in
 let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
 in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"
-lemma action_lemma [simp]:
-"rec_eval rec_action [m, q, c] = Action m q c"
-by (simp add: rec_action_def)
 definition
 "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])
 (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"
-lemma newstat_lemma [simp]:
-"rec_eval rec_newstat [n, c] = Newstat n c"
-apply(simp add: rec_newstat_def)
-apply(case_tac c)
-apply(simp_all)
-done
 definition
 "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in
 let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
 in CN rec_if [cond, if_branch, Z])"
-lemma newstate_lemma [simp]:
-"rec_eval rec_newstate [m, q, r] = Newstate m q r"
-by (simp add: rec_newstate_def)
 definition
 "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"
-lemma conf_lemma [simp]:
-"rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
-by(simp add: rec_conf_def)
 definition
 "rec_state = CN rec_ldec [Id 1 0, Z]"
 definition
 "rec_left = CN rec_ldec [Id 1 0, constn 1]"
 definition
 "rec_right = CN rec_ldec [Id 1 0, constn 2]"
-lemma state_lemma [simp]:
-"rec_eval rec_state [cf] = State cf"
-by (simp add: rec_state_def)
-lemma left_lemma [simp]:
-"rec_eval rec_left [cf] = Left cf"
-by (simp add: rec_left_def)
-lemma right_lemma [simp]:
-"rec_eval rec_right [cf] = Right cf"
-by (simp add: rec_right_def)
 definition
 "rec_step = (let left = CN rec_left [Id 2 0] in
 let right = CN rec_right [Id 2 0] in
 let state = CN rec_state [Id 2 0] in
 let newstate = CN rec_newstate [Id 2 1, state, read] in
 let newleft = CN rec_newleft [left, right, action] in
 let newright = CN rec_newright [left, right, action]
 in CN rec_conf [newstate, newleft, newright])"
-lemma step_lemma [simp]:
+definition
-"rec_eval rec_step [cf, m] = Step cf m"
+"rec_steps = PR (Id 3 0) (CN rec_step [Id 4 1, Id 4 3])"
-by (simp add: Let_def rec_step_def)
-definition
-"rec_steps = PR (Id 3 0)
-(CN rec_step [Id 4 1, Id 4 3])"
-lemma steps_lemma [simp]:
-"rec_eval rec_steps [n, cf, p] = Steps cf p n"
-by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
 definition
 "rec_stknum = CN rec_minus
 [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
 CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
-lemma stknum_lemma [simp]:
-"rec_eval rec_stknum [z] = Stknum z"
-by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
 definition
 "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
 let cond1 = CN rec_le [constn 1, Id 2 0] in
 let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
 definition
 "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
 in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
-lemma left_std_lemma [simp]:
-"rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
-by (simp add: Let_def rec_left_std_def left_std_def)
-lemma right_std_lemma [simp]:
-"rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
-by (simp add: Let_def rec_right_std_def right_std_def)
 definition
 "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
 CN rec_right_std [CN rec_right [Id 1 0]]]"
 definition
 definition
 "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
 CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
-lemma std_lemma [simp]:
-"rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
-by (simp add: rec_std_def)
-lemma final_lemma [simp]:
-"rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
-by (simp add: rec_final_def)
-lemma stop_lemma [simp]:
-"rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
-by (simp add: Let_def rec_stop_def)
 definition
 "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
-lemma halt_lemma [simp]:
-"rec_eval rec_halt [m, cf] = Halt m cf"
-by (simp add: rec_halt_def del: Stop.simps)
 definition
 "rec_uf = CN rec_pred
 [CN rec_stknum
 [CN rec_right
 [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
+lemma read_lemma [simp]:
+"rec_eval rec_read [x] = Read x"
+by (simp add: rec_read_def)
+lemma write_lemma [simp]:
+"rec_eval rec_write [x, y] = Write x y"
+by (simp add: rec_write_def)
+lemma newleft_lemma [simp]:
+"rec_eval rec_newleft [p, r, a] = Newleft p r a"
+by (simp add: rec_newleft_def Let_def)
+lemma newright_lemma [simp]:
+"rec_eval rec_newright [p, r, a] = Newright p r a"
+by (simp add: rec_newright_def Let_def)
+lemma act_lemma [simp]:
+"rec_eval rec_actn [n, c] = Actn n c"
+apply(simp add: rec_actn_def)
+apply(case_tac c)
+apply(simp_all)
+done
+lemma action_lemma [simp]:
+"rec_eval rec_action [m, q, c] = Action m q c"
+by (simp add: rec_action_def)
+lemma newstat_lemma [simp]:
+"rec_eval rec_newstat [n, c] = Newstat n c"
+apply(simp add: rec_newstat_def)
+apply(case_tac c)
+apply(simp_all)
+done
+lemma newstate_lemma [simp]:
+"rec_eval rec_newstate [m, q, r] = Newstate m q r"
+by (simp add: rec_newstate_def)
+lemma conf_lemma [simp]:
+"rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
+by(simp add: rec_conf_def)
+lemma state_lemma [simp]:
+"rec_eval rec_state [cf] = State cf"
+by (simp add: rec_state_def)
+lemma left_lemma [simp]:
+"rec_eval rec_left [cf] = Left cf"
+by (simp add: rec_left_def)
+lemma right_lemma [simp]:
+"rec_eval rec_right [cf] = Right cf"
+by (simp add: rec_right_def)
+lemma step_lemma [simp]:
+"rec_eval rec_step [cf, m] = Step cf m"
+by (simp add: Let_def rec_step_def)
+lemma steps_lemma [simp]:
+"rec_eval rec_steps [n, cf, p] = Steps cf p n"
+by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
+lemma stknum_lemma [simp]:
+"rec_eval rec_stknum [z] = Stknum z"
+by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
+lemma left_std_lemma [simp]:
+"rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
+by (simp add: Let_def rec_left_std_def left_std_def)
+lemma right_std_lemma [simp]:
+"rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
+by (simp add: Let_def rec_right_std_def right_std_def)
+lemma std_lemma [simp]:
+"rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
+by (simp add: rec_std_def)
+lemma final_lemma [simp]:
+"rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
+by (simp add: rec_final_def)
+lemma stop_lemma [simp]:
+"rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
+by (simp add: Let_def rec_stop_def)
+lemma halt_lemma [simp]:
+"rec_eval rec_halt [m, cf] = Halt m cf"
+by (simp add: rec_halt_def del: Stop.simps)
 lemma uf_lemma [simp]:
 "rec_eval rec_uf [m, cf] = UF m cf"
 by (simp add: rec_uf_def)

changeset 267	28d85e8ff391
parent 266	b1b47d28c295
child 269	fa40fd8abb54