anchor.diff:  // Error unsolved goal 
   let WF_POINTWISE = 
   #if BUGGY
  -  prove((parse_term @"WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool)
  -    ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)"),
  -   STRIP_TAC
  -   |> THEN <| MATCH_MP_TAC(GEN_ALL WF_SUBSET)
  -   |> THEN 
  -   <| EXISTS_TAC
  -          (parse_term @"\(x1,y1) (x2,y2). x1 << x2 \/ (x1:A = x2) /\ (y1:B) <<< (y2:B)")
  -   |> THEN <| CONJ_TAC
  -   |> THENL <| [REWRITE_TAC [FORALL_PAIR_THM]
  -                |> THEN <| CONV_TAC TAUT
  -                MATCH_MP_TAC WF_LEX
  -                |> THEN <| ASM_REWRITE_TAC []])
  +    prove((parse_term @"WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool)
  +      ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)"),
  +        STRIP_TAC
  +        |> THEN <| MATCH_MP_TAC(GEN_ALL WF_SUBSET)
  +        |> THEN <| EXISTS_TAC(parse_term @"\(x1,y1) (x2,y2). x1 << x2 \/ (x1:A = x2) /\ (y1:B) <<< (y2:B)")
  +        |> THEN <| CONJ_TAC
  +        |> THENL <| [REWRITE_TAC [FORALL_PAIR_THM]
  +                     |> THEN <| CONV_TAC TAUT;
  +                     MATCH_MP_TAC WF_LEX
  +                     |> THEN <| ASM_REWRITE_TAC []])
   #else
       Sequent([],parse_term @"WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool) ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)")
   #endif
  +
   (* ------------------------------------------------------------------------- *)
   (* Wellfoundedness properties of natural numbers.                            *)
   (* ------------------------------------------------------------------------- *)
  +
   let WF_num = prove((parse_term @"WF(<)"), REWRITE_TAC [WF_IND; num_WF])
   
  -let WF_REC_num = prove((parse_term @"!H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
  +let WF_REC_num = 
  +    prove((parse_term @"!H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
            ==> ?f:num->A. !n. f n = H f n"), MATCH_ACCEPT_TAC(MATCH_MP WF_REC WF_num))
   
   (* ------------------------------------------------------------------------- *)
   (* Natural number measures (useful in program verification).                 *)
   (* ------------------------------------------------------------------------- *)
  +
   let MEASURE = new_definition(parse_term @"MEASURE m = \x y. m(x) < m(y)")
   
   let WF_MEASURE = 
  
positive.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])
  
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Trivially, a WF relation is irreflexive.                                  *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_REFL = 
      prove((parse_term @"!x:A. WF(<<) ==> ~(x << x)"), 
            GEN_TAC
            |> THEN <| REWRITE_TAC [WF]
            |> THEN <| DISCH_THEN(MP_TAC << SPEC(parse_term @"\y:A. y = x"))
            |> THEN <| REWRITE_TAC []
            |> THEN <| MESON_TAC [])
  
  (* ------------------------------------------------------------------------- *)
  (* Even more trivially, the everywhere-false relation is wellfounded.        *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_FALSE = prove((parse_term @"WF(\x y:A. F)"), REWRITE_TAC [WF])
  
  (* ------------------------------------------------------------------------- *)
  (* Tail recursion.                                                           *)
  (* ------------------------------------------------------------------------- *)
  
  let WF_REC_TAIL = 
      prove((parse_term @"!P g h. ?f:A->B. !x. f x = if P(x) then f(g x) else h x"), 
            let lemma1 = prove((parse_term @"~(P 0) ==> ((?n. P(SUC n)) <=> (?n. P(n)))"), MESON_TAC [num_CASES; NOT_SUC])
            let lemma2 = 
                prove((parse_term @"(P 0) ==> ((!m. m < n ==> P(SUC m)) <=> (!m. m < SUC n ==> P(m)))"), 
                      REPEAT(DISCH_TAC
                             |> ORELSE <| EQ_TAC)
                      |> THEN <| INDUCT_TAC
                      |> THEN <| ASM_MESON_TAC [LT_SUC; LT_0])
            REPEAT GEN_TAC
            |> THEN <| MP_TAC(GEN (parse_term @"x:A") (ISPECL [(parse_term @"x:A");
                                                               (parse_term @"\y:A n:num. g(y):A")] num_RECURSION))
            |> THEN <| REWRITE_TAC [SKOLEM_THM; FORALL_AND_THM]
            |> THEN <| DISCH_THEN(X_CHOOSE_THEN (parse_term @"s:A->num->A") STRIP_ASSUME_TAC)
            |> THEN <| EXISTS_TAC(parse_term @"\x:A. if ?n:num. ~P(s x n)
                       then (h:A->B)(@y. ?n. (y = s x n) /\ ~P(s x n) /\
                                             !m. m < n ==> P(s x m))
                       else something_arbitrary:B")
            |> THEN <| X_GEN_TAC(parse_term @"x:A")
            |> THEN <| SUBGOAL_THEN (parse_term @"!n x:A. s (g x) n :A = s x (SUC n)") ASSUME_TAC
            |> THENL <| [INDUCT_TAC
                         |> THEN <| ASM_REWRITE_TAC [];
                         UNDISCH_THEN (parse_term @"!x:A n. s x (SUC n) :A = g (s x n)") (K ALL_TAC)]
            |> THEN <| ASM_CASES_TAC(parse_term @"(P:A->bool) x")
            |> THEN <| ASM_REWRITE_TAC []
            |> THENL <| [ASM_SIMP_TAC [lemma1]
                         |> THEN <| COND_CASES_TAC
                         |> THEN <| ASM_REWRITE_TAC []
                         |> THEN <| CONV_TAC SYM_CONV
                         |> THEN <| ASM_SIMP_TAC [lemma2; lemma1];
                         COND_CASES_TAC
                         |> THENL <| [ALL_TAC;
                                      ASM_MESON_TAC []]
                         |> THEN <| AP_TERM_TAC
                         |> THEN <| MATCH_MP_TAC SELECT_UNIQUE
                         |> THEN <| REWRITE_TAC []
                         |> THEN <| X_GEN_TAC(parse_term @"y:A")
                         |> THEN <| EQ_TAC
                         |> THENL <| [SIMP_TAC [LEFT_IMP_EXISTS_THM]
                                      |> THEN <| INDUCT_TAC
                                      |> THEN <| ASM_REWRITE_TAC []
                                      |> THEN <| ASM_MESON_TAC [LT_0];
                                      ASM_MESON_TAC [LT]]])
  
  (* ------------------------------------------------------------------------- *)
  (* A more general mix of tail and wellfounded recursion.                     *)
  