IndisputableMonolith.Verification.Necessity.FibSubst

declarations in this module (20)

• abbrev Word L10
• def fib L13
• def fibSub L19
• def fibSubWord L24
• def countFalse L27
• def countTrue L32
• lemma countFalse_nil L36
• lemma countTrue_nil L37
• lemma countFalse_cons_false L39
• lemma countFalse_cons_true L43
• lemma countTrue_cons_false L47
• lemma countTrue_cons_true L51
• lemma countFalse_append L55
• lemma countTrue_append L64
• lemma counts_sub_false L74
• lemma counts_sub_true L78
• lemma counts_sub_word L83
• def iter L106
• lemma counts_iter_succ L108
• lemma counts_iter_fib L119