changeset 557 | 812e5d112f49 |
parent 553 | 0f00d440f484 |
child 558 | 671a83abccf3 |
--- a/thys3/BlexerSimp.thy Wed Jun 29 12:38:05 2022 +0100 +++ b/thys3/BlexerSimp.thy Fri Jul 01 13:02:15 2022 +0100 @@ -276,9 +276,12 @@ by simp lemma ss6_realistic: - shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs2)))))" - - + shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs1)))))" + apply(induct rs2 arbitrary: rs1) + apply simp + apply(rename_tac cc cc') + + sorry