equal
deleted
inserted
replaced
45 | termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); |
45 | termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); |
46 rec_exec f (xs @ [r]) = 0; |
46 rec_exec f (xs @ [r]) = 0; |
47 \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
47 \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
48 |
48 |
49 |
49 |
|
50 inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs" |
|
51 |
|
52 inductive_cases terminate_z_reverse[elim!]: "terminate z xs" |
|
53 |
|
54 inductive_cases terminate_s_reverse[elim!]: "terminate s xs" |
|
55 |
|
56 inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs" |
|
57 |
|
58 inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs" |
|
59 |
|
60 inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs" |
|
61 |
50 end |
62 end |