Commit 2023-06-26 14:58 29eff09e

View on Github →

feat: port Archive.MiuLanguage.DecisionSuf (#5475)

Estimated changes

Modified Archive.lean

Created Archive/MiuLanguage/DecisionSuf.lean

added theorem Miu.add_mod2

added theorem Miu.base_case_suf

added theorem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem

added theorem Miu.der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append

added theorem Miu.der_of_decstr

added theorem Miu.der_of_der_append_replicate_U_even

added theorem Miu.der_replicate_I_of_mod3

added theorem Miu.eq_append_cons_U_of_count_U_pos

added theorem Miu.ind_hyp_suf

added theorem Miu.le_pow2_and_pow2_eq_mod3

added theorem Miu.mem_of_count_U_eq_succ

added theorem Miu.replicate_pow_minus_append