equal
deleted
inserted
replaced
116 note Inr' = this |
116 note Inr' = this |
117 show ?thesis |
117 show ?thesis |
118 proof (cases "mrec b h1") |
118 proof (cases "mrec b h1") |
119 case (Some result) |
119 case (Some result) |
120 then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce |
120 then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce |
121 moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" |
121 moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" |
122 apply (intro 1(2)) |
122 apply (intro 1(2)) |
123 apply (auto simp add: Inr Inl') |
123 apply (auto simp add: Inr Inl') |
124 done |
124 done |
125 moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3) |
125 moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3) |
126 ultimately show ?thesis |
126 ultimately show ?thesis |