proposition: Lemma McCarthy_fix_post : (forall n, mcCarthy n = McCarthy mcCarthy n) /\ (forall n, McCarthy_post n (mcCarthy n)).
proof: Proof. Proof using. sets meas: (fun n => If n > 100 then 0 else 101 - n). applys~ (FixFun_fix_inv (measure meas)). introv IH. unfold McCarthy. unfold McCarthy_post. case_if~. forwards [K1 K2]: IH (x+11). unfold measure, meas. case_if; case_if*. rewrite <- K1 in *. sets y: (f1(x+11)). unfolds in K2. forwards [L1 L2]: IH y. unfold measure, meas. case_if; case_if*. case_if*. rewrite <- L1 in *. sets z: (f1 y). unfolds in L2. split~. case_if*. case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat