anchor.diff:                      (\u v. ?t. _GUARDED_PATTERN (GEQ (pat t) u)
                                                   (q x t)
                                                   (GEQ (f(arg x t)) v)))"),
  -  REPEAT GEN_TAC |>THEN<| STRIP_TAC |>THEN<|
  -  REWRITE_TAC[superadmissible] |>THEN<| DISCH_TAC |>THEN<|
  -  REWRITE_TAC[_GUARDED_PATTERN; GEQ_DEF; _MATCH] |>THEN<|
  -  REWRITE_TAC[tailadmissible] |>THEN<|
  -  SUBGOAL_THEN
  -   (parse_term @"!f:A->B x:P.
  +          REPEAT GEN_TAC
  +          |> THEN <| STRIP_TAC
  +          |> THEN <| REWRITE_TAC [superadmissible]
  +          |> THEN <| DISCH_TAC
  +          |> THEN <| REWRITE_TAC [_GUARDED_PATTERN; GEQ_DEF; _MATCH]
  +          |> THEN <| REWRITE_TAC [tailadmissible]
  +          |> THEN <| SUBGOAL_THEN (parse_term @"!f:A->B x:P.
        p f x ==> ((?!v. ?t:Q. pat t:D = e x /\ q x t /\ f(arg x t) = v) <=>
                   ?t. pat t = e x /\ q x t)")
  -   (fun th -> SIMP_TAC[th]) |>THENL<| [ASM_MESON_TAC[]; ALL_TAC] |>THEN<|
  -  MAP_EVERY EXISTS_TAC
  -   [(parse_term @"\(f:A->B) x:P. p f x /\ ?t:Q. pat t:D = e x /\ q x t");
  -    (parse_term @"\f:A->B x:P. arg x (@t. (pat:Q->D) t = e x /\ q x t):A");
  -    (parse_term @"\(f:A->B) x:P. (@z:B. F)")] |>THEN<|
  -  RULE_ASSUM_TAC(REWRITE_RULE[admissible]) |>THEN<| SIMP_TAC[] |>THEN<|
  -  ASM_MESON_TAC[])
  +                (fun th -> SIMP_TAC [th])
  +          |> THENL <| [ASM_MESON_TAC [];
  +                       ALL_TAC]
  +          |> THEN <| MAP_EVERY EXISTS_TAC [(parse_term @"\(f:A->B) x:P. p f x /\ ?t:Q. pat t:D = e x /\ q x t");
  +                                           (parse_term @"\f:A->B x:P. arg x (@t. (pat:Q->D) t = e x /\ q x t):A");
  +                                           (parse_term @"\(f:A->B) x:P. (@z:B. F)")]
  +          |> THEN <| RULE_ASSUM_TAC(REWRITE_RULE [admissible])
  +          |> THEN <| SIMP_TAC []
  +          |> THEN <| ASM_MESON_TAC [])
   
   (* ------------------------------------------------------------------------- *)
   (* Combine general WF/tail recursion theorem with casewise definitions.      *)
   (* ------------------------------------------------------------------------- *)
   
   let WF_REC_TAIL_GENERAL' = 
  - prove ((parse_term @"!P G H H'.
  +    prove((parse_term @"!P G H H'.
            WF (<<) /\
            (!f g x. (!z. z << x ==> (f z = g z))
                     ==> (P f x <=> P g x) /\
  
positive.code:              (\f x:P. _GUARDED_PATTERN (GEQ (pat f x) (e f x))
                                         (q f x)
                                         (GEQ (t f x) (y f x)))"),
    REPEAT GEN_TAC |>THEN<|
    REWRITE_TAC[admissible; FORALL_PAIR_THM; _GUARDED_PATTERN] |>THEN<|
    REWRITE_TAC[GEQ_DEF] |>THEN<| REPEAT STRIP_TAC |>THEN<|
    REPEAT(MATCH_MP_TAC(TAUT (parse_term @"(a <=> a') /\ (a /\ a' ==> (b <=> b'))
                              ==> (a /\ b <=> a' /\ b')")) |>THEN<|
           REPEAT STRIP_TAC) |>THEN<|
    TRY(MATCH_MP_TAC(MESON[] (parse_term @"x = x' /\ y = y' ==> (x = y <=> x' = y')"))) |>THEN<|
    ASM_MESON_TAC[])
  
  let ADMISSIBLE_NSUM = 
   prove ((parse_term @"!(<<) p:(B->C)->P->bool s:P->A h a b.
          admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
                         (\(k,x). s x) (\f (k,x). h f x k)
     ==> admissible(<<) p s (\f x. nsum(a(x)..b(x)) (h f x))"),
    REWRITE_TAC[admissible; FORALL_PAIR_THM] |>THEN<| REPEAT STRIP_TAC |>THEN<|
    MATCH_MP_TAC NSUM_EQ_NUMSEG |>THEN<| ASM_MESON_TAC[])
  
  let ADMISSIBLE_SUM = 
   prove ((parse_term @"!(<<) p:(B->C)->P->bool s:P->A h a b.
          admissible(<<) (\f (k,x). a(x) <= k /\ k <= b(x) /\ p f x)
                         (\(k,x). s x) (\f (k,x). h f x k)
     ==> admissible(<<) p s (\f x. sum(a(x)..b(x)) (h f x))"),
    REWRITE_TAC[admissible; FORALL_PAIR_THM] |>THEN<| REPEAT STRIP_TAC |>THEN<|
    MATCH_MP_TAC SUM_EQ_NUMSEG |>THEN<| ASM_MESON_TAC[])
  
  let ADMISSIBLE_MAP = 
   prove ((parse_term @"!(<<) p s h l.
          admissible(<<) p s l /\
          admissible (<<) (\f (y,x). p f x /\ MEM y (l f x))
                          (\(y,x). s x) (\f (y,x). h f x y)
     ==> admissible (<<) p s (\f:A->B x:P. MAP (h f x) (l f x))"),
    REWRITE_TAC[admissible; FORALL_PAIR_THM] |>THEN<| REPEAT STRIP_TAC |>THEN<|
    MATCH_MP_TAC(MESON[] (parse_term @"x = y /\ MAP f x = MAP g x ==> MAP f x = MAP g y")) |>THEN<|
    CONJ_TAC |>THENL<| [ASM_MESON_TAC[]; ALL_TAC] |>THEN<|
    MATCH_MP_TAC MAP_EQ |>THEN<| REWRITE_TAC[GSYM ALL_MEM] |>THEN<|
    REPEAT STRIP_TAC |>THEN<| FIRST_X_ASSUM MATCH_MP_TAC |>THEN<|
    ASM_REWRITE_TAC[FORALL_PAIR_THM] |>THEN<| ASM_MESON_TAC[])
  
  let ADMISSIBLE_MATCH_SEQPATTERN = 
   prove ((parse_term @"!(<<) p s c1 c2 e.
          admissible(<<) p s (\f x. ?y. c1 f x (e f x) y) /\
          admissible(<<) (\f x. p f x /\ ?y. c1 f x (e f x) y) s
                         (\f x. _MATCH (e f x) (c1 f x)) /\
  
negative.code: open FSharp.Compatibility.OCaml.Num
  
  open ExtCore.Control
  open ExtCore.Control.Collections
  
  open NHol
  open lib
  