equal
deleted
inserted
replaced
638 apply (smt (verit) fuse.elims lessI less_Suc_eq plus_1_eq_Suc s_complexity.simps(2) s_complexity.simps(3) s_complexity.simps(4) s_complexity.simps(5) s_complexity.simps(6) s_complexity.simps(7)) |
638 apply (smt (verit) fuse.elims lessI less_Suc_eq plus_1_eq_Suc s_complexity.simps(2) s_complexity.simps(3) s_complexity.simps(4) s_complexity.simps(5) s_complexity.simps(6) s_complexity.simps(7)) |
639 apply simp |
639 apply simp |
640 sorry |
640 sorry |
641 |
641 |
642 |
642 |
643 lemma compl_rrewrite_down1: |
643 lemma compl_rrewrite_down1_1: |
644 shows "\<lbrakk>r1 \<le>1 r2; s_complexity r1 = s_complexity r2 \<rbrakk> \<Longrightarrow> r1 = r2" |
644 shows "\<lbrakk>r1 \<le>1 r2; s_complexity r1 = s_complexity r2 \<rbrakk> \<Longrightarrow> r1 = r2" |
645 using compl_rrewrite_down nat_less_le by auto |
645 using compl_rrewrite_down nat_less_le by auto |
646 |
646 |
647 |
647 |
648 |
648 |