anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Some preservation theorems for wellfoundedness.                           *)
   (* ------------------------------------------------------------------------- *)
  +
   let WF_SUBSET = 
       prove
           ((parse_term @"(!(x:A) y. x << y ==> x <<< y) /\ WF(<<<) ==> WF(<<)"), 
  
positive.code: 
  open FSharp.Compatibility.OCaml
  open FSharp.Compatibility.OCaml.Num
  
  open NHol
  open lib
  
negative.code:            |> THEN <| ASM_REWRITE_TAC [])
  
  let WF_REC_WF = 
      prove((parse_term @"(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
                   ==> ?f:A->num. !x. f x = H f x)
      ==> WF(<<)"),
            DISCH_TAC
            |> THEN <| REWRITE_TAC [WF_DCHAIN]
            |> THEN <| DISCH_THEN(X_CHOOSE_TAC(parse_term @"x:num->A"))
            |> THEN <| SUBGOAL_THEN (parse_term @"!n. (x:num->A)(@m. x(m) << x(n)) << x(n)") ASSUME_TAC
            |> THENL <| [CONV_TAC(BINDER_CONV SELECT_CONV)
                         |> THEN <| ASM_MESON_TAC [];
                         ALL_TAC]
            |> THEN <| FIRST_ASSUM(MP_TAC << SPEC(parse_term @"\f:A->num. \y:A. if ?p:num. y = x(p)
                         then SUC(f(x(@m. x(m) << y)))
                         else 0")) 
            |> THEN <| REWRITE_TAC [NOT_IMP]
            |> THEN <| CONJ_TAC
            |> THENL <| [REPEAT STRIP_TAC
                         |> THEN <| COND_CASES_TAC
                         |> THEN <| REWRITE_TAC []
                         |> THEN <| FIRST_ASSUM(X_CHOOSE_THEN (parse_term @"p:num") SUBST_ALL_TAC)
                         |> THEN <| AP_TERM_TAC
                         |> THEN <| FIRST_ASSUM MATCH_MP_TAC
                         |> THEN <| FIRST_ASSUM MATCH_ACCEPT_TAC;
                         ALL_TAC]
            |> THEN <| DISCH_THEN(X_CHOOSE_THEN (parse_term @"f:A->num") MP_TAC)
            |> THEN <| DISCH_THEN(MP_TAC << GEN(parse_term @"n:num") << SPEC(parse_term @"(x:num->A) n"))
            |> THEN <| SUBGOAL_THEN (parse_term @"!n. ?p. (x:num->A) n = x p") (fun th -> REWRITE_TAC [th])
            |> THENL <| [MESON_TAC [];
                         DISCH_TAC]
            |> THEN <| SUBGOAL_THEN (parse_term @"!n:num. ?k. f(x(k):A) < f(x(n))") ASSUME_TAC
            |> THENL <| [GEN_TAC
                         |> THEN <| EXISTS_TAC(parse_term @"@m:num. x(m):A << x(n)")
                         |> THEN <| FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [th])
                         |> THEN <| REWRITE_TAC [LT];
                         MP_TAC(SPEC (parse_term @"\n:num. ?i:num. n = f(x(i):A)") num_WOP)
                         |> THEN <| REWRITE_TAC []
                         |> THEN <| ASM_MESON_TAC []])
  
  (* ------------------------------------------------------------------------- *)
  (* Combine the two versions of the recursion theorem.                        *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_EREC = 
      prove((parse_term @"WF(<<) ==>
          !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
               ==> ?!f:A->B. !x. f x = H f x"), MESON_TAC [WF_REC; WF_UREC])
  
  