anchor.diff:  
   open FSharp.Compatibility.OCaml
   open FSharp.Compatibility.OCaml.Num
  +
  +open ExtCore.Control
   
   open NHol
   open lib
  
positive.code: (* ------------------------------------------------------------------------- *)
  (* Some preservation theorems for wellfoundedness.                           *)
  (* ------------------------------------------------------------------------- *)
  let WF_SUBSET = 
      prove
          ((parse_term @"(!(x:A) y. x << y ==> x <<< y) /\ WF(<<<) ==> WF(<<)"), 
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Equivalence of the "infinite descending chains" version.                  *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_DCHAIN = 
      prove((parse_term @"WF(<<) <=> ~(?s:num->A. !n. s(SUC n) << s(n))"), 
            REWRITE_TAC [WF;
                         TAUT(parse_term @"(a <=> ~b) <=> (~a <=> b)");
                         NOT_FORALL_THM]
            |> THEN <| EQ_TAC
            |> THEN <| DISCH_THEN CHOOSE_TAC
            |> THENL <| [POP_ASSUM(MP_TAC << REWRITE_RULE [NOT_IMP])
                         |> THEN <| DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC(parse_term @"a:A")) ASSUME_TAC)
                         |> THEN <| SUBGOAL_THEN (parse_term @"!x:A. ?y. P(x) ==> P(y) /\ y << x") MP_TAC
                         |> THENL <| [ASM_MESON_TAC [];
                                      REWRITE_TAC [SKOLEM_THM]]
                         |> THEN <| DISCH_THEN(X_CHOOSE_THEN (parse_term @"f:A->A") STRIP_ASSUME_TAC)
                         |> THEN <| CHOOSE_TAC
                                        (prove_recursive_functions_exist num_RECURSION 
                                             (parse_term @"(s(0) = a:A) /\ (!n. s(SUC n) = f(s n))"))
                         |> THEN <| EXISTS_TAC(parse_term @"s:num->A")
                         |> THEN <| ASM_REWRITE_TAC []
                         |> THEN <| SUBGOAL_THEN (parse_term @"!n. P(s n) /\ s(SUC n):A << s(n)") (fun th -> ASM_MESON_TAC [th])
                         |> THEN <| INDUCT_TAC
                         |> THEN <| ASM_REWRITE_TAC []
                         |> THEN <| ASM_MESON_TAC [];
  
                         EXISTS_TAC(parse_term @"\y:A. ?n:num. y = s(n)")
                         |> THEN <| REWRITE_TAC []
                         |> THEN <| ASM_MESON_TAC []])
  
  (* ------------------------------------------------------------------------- *)
  (* Equivalent to just *uniqueness* part of recursion.                        *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_UREC = 
      prove((parse_term @"WF(<<) ==>
          !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
               ==> !(f:A->B) g. (!x. f x = H f x) /\ (!x. g x = H g x)
                                 ==> (f = g)"),
          REWRITE_TAC [WF_IND]
          |> THEN <| REPEAT STRIP_TAC
          |> THEN <| REWRITE_TAC [FUN_EQ_THM]
          |> THEN <| FIRST_ASSUM MATCH_MP_TAC
          |> THEN <| GEN_TAC
          |> THEN <| DISCH_THEN(ANTE_RES_THEN MP_TAC)
          |> THEN <| ASM_REWRITE_TAC [])
  
  let WF_UREC_WF = 
      prove((parse_term @"(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
           ==> !(f:A->bool) g. (!x. f x = H f x) /\ (!x. g x = H g x)
                             ==> (f = g))
      ==> WF(<<)"),
            REWRITE_TAC [WF_IND]
            |> THEN <| DISCH_TAC
            |> THEN <| GEN_TAC
            |> THEN <| DISCH_TAC
            |> THEN <| FIRST_X_ASSUM(MP_TAC << SPEC(parse_term @"\f x. P(x:A) \/ !z:A. z << x ==> f(z)"))
            |> THEN <| REWRITE_TAC []
            |> THEN <| W(C SUBGOAL_THEN (fun t -> REWRITE_TAC [t]) << funpow 2 (Choice.get << lhand) << snd)
            |> THENL <| [MESON_TAC [];
                         DISCH_THEN(MP_TAC << SPECL [(parse_term @"P:A->bool");
                                                     (parse_term @"\x:A. T")])
                         |> THEN <| REWRITE_TAC [FUN_EQ_THM]
                         |> THEN <| ASM_MESON_TAC []])
  
  (* ------------------------------------------------------------------------- *)
  (* Stronger form of recursion with "inductive invariant" (Krstic/Matthews).  *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_REC_INVARIANT = 
      prove((parse_term @"WF(<<)
      ==> !H S. (!f g x. (!z. z << x ==> (f z = g z) /\ S z (f z))
                         ==> (H f x = H g x) /\ S x (H f x))
                ==> ?f:A->B. !x. (f x = H f x)"),
            let lemma = 
                prove_inductive_relations_exist(parse_term @"!f:A->B x. (!z. z << x ==> R z (f z)) ==> R x (H f x)")
            REWRITE_TAC [WF_IND]
            |> THEN <| REPEAT STRIP_TAC
            |> THEN <| X_CHOOSE_THEN (parse_term @"R:A->B->bool") STRIP_ASSUME_TAC lemma
            |> THEN <| SUBGOAL_THEN (parse_term @"!x:A. ?!y:B. R x y") (fun th -> ASM_MESON_TAC [th])
            |> THEN <| FIRST_X_ASSUM MATCH_MP_TAC
            |> THEN <| REPEAT STRIP_TAC
            |> THEN <| FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [th])
            |> THEN <| SUBGOAL_THEN (parse_term @"!x:A y:B. R x y ==> S x y") MP_TAC
            |> THEN <| ASM_MESON_TAC [])
  
  (* ------------------------------------------------------------------------- *)
  (* Equivalent to just *existence* part of recursion.                         *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_REC = 
      prove((parse_term @"WF(<<)
      ==> !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
  