equal
deleted
inserted
replaced
457 lemma bintrunc_Suc_lem: |
457 lemma bintrunc_Suc_lem: |
458 "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" |
458 "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" |
459 by auto |
459 by auto |
460 |
460 |
461 lemmas bintrunc_Suc_Ialts = |
461 lemmas bintrunc_Suc_Ialts = |
462 bintrunc_Min_I bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard] |
462 bintrunc_Min_I [THEN bintrunc_Suc_lem, standard] |
|
463 bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard] |
463 |
464 |
464 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
465 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
465 |
466 |
466 lemmas sbintrunc_Suc_Is = |
467 lemmas sbintrunc_Suc_Is = |
467 sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard] |
468 sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard] |