anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Definition of wellfoundedness for arbitrary (infix) relation <<           *)
   (* ------------------------------------------------------------------------- *)
  +
   let WF = 
       new_definition
           (parse_term @"WF(<<) <=> !P:A->bool. (?x. P(x)) ==> (?x. P(x) /\ !y. y << x ==> ~P(y))")
  
positive.code:          |> THEN <| MESON_TAC [])
  
  let WF_MEASURE_GEN = 
      prove
          ((parse_term @"!m:A->B. WF(<<) ==> WF(\x x'. m x << m x')"), 
           GEN_TAC
           |> THEN <| REWRITE_TAC [WF_IND]
           |> THEN <| REPEAT STRIP_TAC
           |> THEN 
           <| FIRST_ASSUM
                  (MP_TAC << SPEC(parse_term @"\y:B. !x:A. (m(x) = y) ==> P x"))
           |> THEN 
           <| UNDISCH_TAC
                  (parse_term @"!x. (!y. (m:A->B) y << m x ==> P y) ==> P x")
           |> THEN <| REWRITE_TAC []
           |> THEN <| MESON_TAC [])
  
  // Error too deep
  let WF_LEX_DEPENDENT = 
  #if BUGGY
      prove((parse_term @"!R:A->A->bool S:A->B->B->bool. WF(R) /\ (!a. WF(S a))
            ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S r1 s1 s2)"),
           REPEAT GEN_TAC
           |> THEN <| REWRITE_TAC [WF]
           |> THEN <| STRIP_TAC
           |> THEN <| X_GEN_TAC(parse_term @"P:A#B->bool")
           |> THEN <| REWRITE_TAC [LEFT_IMP_EXISTS_THM]
           |> THEN <| GEN_REWRITE_TAC I [FORALL_PAIR_THM]
           |> THEN <| MAP_EVERY X_GEN_TAC [(parse_term @"a0:A")
                                           (parse_term @"b0:B")]
           |> THEN <| DISCH_TAC
           |> THEN 
           <| FIRST_X_ASSUM(MP_TAC << SPEC(parse_term @"\a:A. ?b:B. P(a,b)"))
           |> THEN <| REWRITE_TAC [LEFT_IMP_EXISTS_THM]
           |> THEN <| DISCH_THEN(MP_TAC << SPECL [(parse_term @"a0:A")
                                                  (parse_term @"b0:B")])
           |> THEN <| ASM_REWRITE_TAC []
           |> THEN 
           <| DISCH_THEN
                  (X_CHOOSE_THEN (parse_term @"a:A") 
                       (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC))
           |> THEN <| DISCH_THEN(X_CHOOSE_TAC(parse_term @"b1:B"))
           |> THEN 
           <| FIRST_X_ASSUM
                  (MP_TAC << SPECL [(parse_term @"a:A")
                                    (parse_term @"\b. (P:A#B->bool) (a,b)")])
           |> THEN <| REWRITE_TAC [LEFT_IMP_EXISTS_THM]
           |> THEN <| DISCH_THEN(MP_TAC << SPEC(parse_term @"b1:B"))
           |> THEN <| ASM_REWRITE_TAC []
           |> THEN 
           <| DISCH_THEN
                  (X_CHOOSE_THEN (parse_term @"b:B") 
                       (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC))
           |> THEN <| DISCH_TAC
           |> THEN <| EXISTS_TAC(parse_term @"(a:A,b:B)")
           |> THEN <| ASM_REWRITE_TAC []
           |> THEN <| REWRITE_TAC [FORALL_PAIR_THM]
           |> THEN <| ASM_MESON_TAC [])
  #else
      Choice.result <| Sequent([], parse_term @"!R:A->A->bool S:A->B->B->bool. WF(R) /\ (!a. WF(S a)) 
          ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S r1 s1 s2)") : thm
  
negative.code: // 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 []])
  #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))
           ==> ?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 = 
  