| changeset 601 | ce4e5151a836 |
| parent 600 | fd068f39ac23 |
| child 618 | 233cf2b97d1a |
| 600:fd068f39ac23 | 601:ce4e5151a836 |
|---|---|
617 apply simp |
617 apply simp |
618 using prf22 apply blast |
618 using prf22 apply blast |
619 by (simp add: scomp_size_reduction) |
619 by (simp add: scomp_size_reduction) |
620 |
620 |
621 lemma leq1_eq1_equal: |
621 lemma leq1_eq1_equal: |
622 shows "\<lbrakk>r1 \<le>1 r2; |
622 shows "\<lbrakk>r1 \<le>1 r2; bsimp r2 = r1 \<rbrakk> \<Longrightarrow> r1 = r2 \<or> s_complexity r1 < s_complexity r2" |
623 sorry |
|
623 |
624 |
624 |
625 |
625 |
626 |
626 |
627 |
627 |
628 |