equal
deleted
inserted
replaced
33 | termi_s: "terminate s [n]" |
33 | termi_s: "terminate s [n]" |
34 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
34 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
35 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
35 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
36 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
36 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
37 | termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)" |
37 | termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)" |
38 | termi_pr_suc: "\<lbrakk>terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> |
38 | termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); length xs = n; |
|
39 terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> |
39 \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)" |
40 \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)" |
40 | termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0; |
41 | termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0; |
41 \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
42 \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
42 |
43 |
43 end |
44 end |