Theory SMT_Internals_Regressions

theory SMT_Internals_Regressions
  imports HOL.SMT
begin

(* Test smtlib.ML *)
(* Purely syntactical testing! *)

ML‹
exception SMT_Regression of string

(*expects a string, a SMTLIB.tree and a boolean expressing if the string should be parsed into 
the tree or not.*)
fun expect_parsing_error str =
  str |> single |> Timeout.apply (seconds 5.0) SMTLIB.parse |> K (raise (SMT_Regression ("Input expected to raise parsing error but did not: " ^ str)))
  handle SMTLIB.PARSE(_,_) => true

(*expects a string, a SMTLIB.tree and a boolean expressing if the string should be parsed into 
the tree or not.*)
fun check_tree str tree expected_value =
let
  val tree' = [str] |> SMTLIB.parse |> @{print}
  val match = (expected_value = (tree = tree'))
val _ = (tree', tree) |> @{print}
in 
 case match of
  true => true |
  false => raise (SMT_Regression ("SMTLIB.parse does not give expected output for " ^ str ^ " instead resulted in " ^ SMTLIB.str_of tree'))
end

(* expects a tree and the string it should be printed as *)
fun check_str_of tree expected =
  let val res = SMTLIB.str_of tree in
    if res = expected then true
    else raise (SMT_Regression ("SMTLIB.str_of gives " ^ quote res ^ " instead of " ^ quote expected))
  end

fun check_dec_to_rat dec expected =
  let
    fun str (i, j) = "(" ^ signed_string_of_int i ^ ", " ^ signed_string_of_int j ^ ")"
    val res = SMTLIB.convert_dec_to_rat dec
  in
    if res = expected then true
    else raise (SMT_Regression ("SMTLIB.convert_dec_to_rat " ^ str dec ^ " gives " ^ str res ^
      " instead of " ^ str expected))
  end


(*Regression Tests*)

val _ = expect_parsing_error "" 
val _ = check_tree "()" (SMTLIB.S []) true


(*Sym*)

val _ = check_tree "x" (SMTLIB.Sym "y") false
val _ = check_tree "x" (SMTLIB.Sym "x") true
val _ = check_tree "(x)" (SMTLIB.Sym "x") false
val _ = check_tree "|x|" (SMTLIB.Sym "x") true
val _ = check_tree "|<|" (SMTLIB.Sym "<") true
val _ = check_tree "@my+var<3" (SMTLIB.Sym "@my+var<3") true
val _ = check_tree "| my test|" (SMTLIB.Sym " my test") true
val _ = check_tree "||" (SMTLIB.Sym "") true

val _ = expect_parsing_error "|s||"


(*Int*)

val _ = check_tree "1" (SMTLIB.Num 1) true
val _ = check_tree "45" (SMTLIB.Num 54) false
val _ = check_tree "00078768" (SMTLIB.Num 78768) true
val _ = check_tree "00078768" (SMTLIB.Num 078768) true
val _ = check_tree "000" (SMTLIB.Num 0) true
val _ = check_tree "-23" (SMTLIB.Num (~23)) true
val _ = check_tree "-23" (SMTLIB.S[SMTLIB.Sym "-", SMTLIB.Num (~23)]) false


(*Dec*)

val _ = check_tree "1/2" (SMTLIB.S [SMTLIB.Sym "/",SMTLIB.Dec (1,0),SMTLIB.Dec (2,0)]) true
val _ = check_tree "01.234" (SMTLIB.Dec (1234,3)) true
val _ = check_tree "01.234" (SMTLIB.Dec (201,234)) false
val _ = check_tree "0.05" (SMTLIB.Dec (5,2)) true
val _ = check_tree "1.05" (SMTLIB.Dec (105,2)) true
val _ = check_tree "0.50" (SMTLIB.Dec (5,1)) true
val _ = check_tree "5.0" (SMTLIB.Dec (5,0)) true
val _ = check_tree "-0.5" (SMTLIB.Dec (~5,1)) true
val _ = check_tree "-1.5" (SMTLIB.Dec (~15,1)) true
val _ = check_tree "-0.05" (SMTLIB.Dec (~5,2)) true
val _ = check_tree "-1.0" (SMTLIB.Dec (~1,0)) true
val _ = check_tree "47/28" (SMTLIB.S [SMTLIB.Sym "/",SMTLIB.Dec (47,0),SMTLIB.Dec (28,0)]) true
val _ = check_tree "-47/28" (SMTLIB.S [SMTLIB.Sym "/",SMTLIB.S[SMTLIB.Sym "-", SMTLIB.Dec (47,0)],SMTLIB.Dec (28,0)]) false
val _ = check_tree "-47/28" (SMTLIB.S [SMTLIB.Sym "/",SMTLIB.Dec (~47,0),SMTLIB.Dec (28,0)]) true
val _ = check_tree "(- 47/28)" (SMTLIB.S[SMTLIB.Sym "-", SMTLIB.S [SMTLIB.Sym "/",SMTLIB.Dec (47,0),SMTLIB.Dec (28,0)]]) true

val _ = check_str_of (SMTLIB.Dec (5,2)) "0.05"
val _ = check_str_of (SMTLIB.Dec (105,2)) "1.05"
val _ = check_str_of (SMTLIB.Dec (5,0)) "5"
val _ = check_str_of (SMTLIB.Dec (~5,1)) "-0.5"
val _ = check_str_of (SMTLIB.Dec (~5,2)) "-0.05"

val _ = expect_parsing_error "01.234.99"
val _ = expect_parsing_error "01."
val _ = expect_parsing_error "47/-28"
val _ = expect_parsing_error "3.2/5"

(*I guess these are allowed?*)
(*val _ = expect_parsing_error ".38"*)
(*val _ = expect_parsing_error "-." *)


(*convert_dec_to_rat*)

val _ = check_dec_to_rat (0, 0) (0, 1)
val _ = check_dec_to_rat (5, 0) (5, 1)
val _ = check_dec_to_rat (5, 1) (5, 10)
val _ = check_dec_to_rat (15, 1) (15, 10)
val _ = check_dec_to_rat (5, 2) (5, 100)
val _ = check_dec_to_rat (1234, 3) (1234, 1000)
val _ = check_dec_to_rat (1025, 2) (1025, 100)

(*Key*)

val _ = check_tree ":hi" (SMTLIB.Key "hi") true
val _ = check_tree ":pattern1" (SMTLIB.Key "hi") false
val _ = expect_parsing_error ": spacebeforepattern"


(*Str*)

val _ = check_tree "\"sdf\"" (SMTLIB.Str "sdf") true
val _ = check_tree "\"\"" (SMTLIB.Str "") true
val _ = check_tree "\" \"" (SMTLIB.Str "") false
val _ = check_tree "\"these should be replaced: \\\\\"" (SMTLIB.Str "these should be replaced: \\") true

val _ = expect_parsing_error "\"notclosed"
val _ = expect_parsing_error "notclosedopen\""


(*BVNum*)

val _ = check_tree "#b0" (SMTLIB.BVNum (0,1)) true
val _ = check_tree "#b00100000101" (SMTLIB.BVNum (261,11)) true


(*S*)
val _ = check_tree "()" (SMTLIB.S []) true
val _ = check_tree "( )" (SMTLIB.S []) true
val _ = check_tree "(op)" (SMTLIB.S [SMTLIB.Sym "op"]) true
val _ = check_tree "(op arg1 arg2)" (SMTLIB.S [SMTLIB.Sym "op",SMTLIB.Sym "arg1",SMTLIB.Sym "arg2"]) true
val _ = expect_parsing_error "(01"

(*forall*)
val _ = check_tree "(forall ((X Int)) (= X 12))"
 (SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S [SMTLIB.S [SMTLIB.Sym "X", SMTLIB.Sym "Int"]],
  SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym "X", SMTLIB.Num 12]]) true
val x = SMTLIB.parse ["(forall ((X Int)) (= (f X) 12))"]
›

declare[[show_hyps]]
(* Test alethe_proof.ML *)
(* Purely syntactical testing! *)


ML‹
exception SMT_Regression of string
open SMTLIB
open Alethe_Proof

(*expects 
a SMTLIB.tree list, and a raw_alethe_node list, and a boolean indicating
if the SMTLIB.tree list should be parsed into a the raw_alethe_node or not.
The current_anchor_id is set to NONE and the name bindings to the empty name bindings
SMTLIB_Proof.empty_name_binding*)
fun expect_parsing_error trees =
   (Timeout.apply (seconds 5.0) parse_raw_proof_steps) NONE trees SMTLIB_Proof.empty_name_binding|> K (raise (SMT_Regression ("Input expected to raise parsing error but did not")))
  handle ALETHE_PROOF_PARSE _ => true |
   Fail _ => true


(*expects a string, a SMTLIB.tree and a boolean expressing if the string should be parsed into 
the tree or not.*)
fun check_raw_node trees raw_node expected_value =
let
  val node = Alethe_Proof.parse_raw_proof_steps NONE trees SMTLIB_Proof.empty_name_binding
  val match = (expected_value = ((fn (a,_,_) => a) node =  raw_node))
  (*val _ = @{print}("node",node)*)
in 
 case match of
  true => true |
  false => raise (SMT_Regression ("Alethe_Proof.parse_raw_proof_steps does not give expected output instead resulted in "))
end

(* expects a string and the numerator/denominator the argument should be extracted to *)
fun check_coefficients str expected =
  let
    fun pair_str (i, j) = "(" ^ signed_string_of_int i ^ ", " ^ signed_string_of_int j ^ ")"
    val res = Alethe_Proof.extract_coefficients (SMTLIB.parse [str])
  in
    if res = expected then true
    else raise (SMT_Regression ("Alethe_Proof.extract_coefficients " ^ str ^ " gives " ^
      pair_str res ^ " instead of " ^ pair_str expected))
  end



(*Regression Tests*)

val missing_concl = SMTLIB.parse ["(step t0  :rule equiv_pos2)"]
val _ = expect_parsing_error [missing_concl]
val missing_id = SMTLIB.parse ["(step (+ 0 1) :rule equiv_pos2)"]
val _ = expect_parsing_error [missing_id]
val invalid_rule = SMTLIB.parse ["(step t0 (+ 0 1) :rule)"]
val _ = expect_parsing_error [invalid_rule]
val missing_rule_name = SMTLIB.parse ["(step t0 (+ 0 1) :rule)"]
val _ = expect_parsing_error [missing_rule_name]
val missing_rule = SMTLIB.parse ["(step t0 (+ 0 1))"]
val _ = expect_parsing_error [missing_rule]
val malformed_args = SMTLIB.parse ["(step t17 (cl) :rule hole :args 0)"]
val _ = expect_parsing_error [malformed_args]


(*steps*)

val testTree = SMTLIB.parse ["(step t99 (cl) :rule resolution)"]
val resTree = 
  Raw_Alethe_Node {concl = Sym "false", context_assignments = [], id = "t99", prems = [],
   rule = "resolution", step_args = [], subproof = [], prop_skeleton = Sym "true"}
val _ = check_raw_node [testTree] [resTree] true

(*Testing step arguments*)


(* No step argument given for argument optional rule *)
val testTree = SMTLIB.parse ["(step t17 (cl (+ @p_517 0)) :rule hole)"]
val resTree = Raw_Alethe_Node
  {concl = S [Sym "or", S [Sym "+", Sym "@p_517",Num 0]], context_assignments = [], id = "t17", 
  prems = [], rule = "hole", step_args = [], subproof = [], prop_skeleton = S [Sym "or", Sym "true"]}
val _ = check_raw_node [testTree] [resTree] true

(* Step argument given but not added *)
val testTree = SMTLIB.parse ["(step t17 (cl) :rule hole :args (0))"]
val resTree = Raw_Alethe_Node
  {concl = Sym "false", context_assignments = [], id = "t17", prems = [], rule = "hole",
   step_args = [], subproof = [], prop_skeleton = Sym "true"}
val _ = check_raw_node [testTree] [resTree] false

(* Step argument given and properly added *)
val testTree = SMTLIB.parse ["(step t17 (cl) :rule hole :args (0))"]
val resTree = Raw_Alethe_Node
 {concl = Sym "false", context_assignments = [], id = "t17", prems = [], rule = "hole", 
  step_args = [Num 0], subproof = [], prop_skeleton = Sym "true"}
val _ = check_raw_node [testTree] [resTree] true

(* Rule does not allow step argument and none given *)
val testTree = SMTLIB.parse ["(step t17 (cl (not (not (not a))) a) :rule not_not)"]
val resTree = Raw_Alethe_Node
  {concl =  S [Sym "or", S [Sym "not", S [Sym "not", S [Sym "not", Sym "a"]]], Sym "a"],
   context_assignments = [], id = "t17", prems = [], rule = "not_not", step_args = [], 
   subproof = [], prop_skeleton = S [Sym "or", Sym "true", Sym "true"]}
val _ = check_raw_node [testTree] [resTree] true

(* Unexpected step argument given TODO*)
val testTree = SMTLIB.parse ["(step t17 (cl (not (not (not a))) a) :rule not_not :args (0))"]
val _ = check_raw_node [testTree] [resTree] false
val resTree = Raw_Alethe_Node
  {concl =  S [Sym "or", S [Sym "not", S [Sym "not", S [Sym "not", Sym "a"]]], Sym "a"], 
   context_assignments = [], id = "t17", prems = [], rule = "not_not", step_args = [Num 0],
   subproof = [], prop_skeleton = S [Sym "or", Sym "true", Sym "true"]}
val x = check_raw_node [testTree] [resTree] true

(* Step argument is string *)
val testTree = SMTLIB.parse ["(step t17 (cl) :rule rare_rewrite :args (\"evaluate\"))"]
val resTree = Raw_Alethe_Node
  {concl = Sym "false", context_assignments = [], id = "t17", prems = [], rule = "rare_rewrite",
   step_args = [Str "evaluate"], subproof = [], prop_skeleton = Sym "true"}
val _ = check_raw_node [testTree] [resTree] true

(* Weird characters in symbol names*)
val testTree = SMTLIB.parse ["(step t17 (cl (exists ((main_~i~6 Int)) (and (<= c_main_~j~6 (+ (* 2 main_~i~6) 2)) (<= main_~i~6 4) (<= main_~i~6 c_main_~k~6)))) :rule rare_rewrite :args (\"evaluate\"))"]
val resTree = Raw_Alethe_Node
      {concl = S [Sym "or",
       S [Sym "exists", S [S [Sym "main_~i~6", Sym "Int"]],
          S [Sym "and", S [Sym "<=", Sym "c_main_~j~6", S [Sym "+", S [Sym "*", Num 2, Sym "main_~i~6"], Num 2]], S [Sym "<=", Sym "main_~i~6", Num 4],
             S [Sym "<=", Sym "main_~i~6", Sym "c_main_~k~6"]]]]
  , context_assignments = [], id = "t17", prems = [], rule = "rare_rewrite", 
  step_args = [Str "evaluate"], subproof = [], prop_skeleton = S [Sym "or", Sym "true"]}
val _ = check_raw_node [testTree] [resTree] true


val testNode = Alethe_Proof.parse_raw_proof_steps NONE [testTree] SMTLIB_Proof.empty_name_binding


(*extract_coefficients*)

val _ = check_coefficients "5" (5, 1)
val _ = check_coefficients "(- 5)" (~5, 1)
val _ = check_coefficients "(/ 1 2)" (1, 2)
val _ = check_coefficients "0.0" (0, 1)
val _ = check_coefficients "5.0" (5, 1)
val _ = check_coefficients "0.5" (5, 10)
val _ = check_coefficients "1.5" (15, 10)
val _ = check_coefficients "10.25" (1025, 100)
val _ = check_coefficients "(- 5.0)" (~5, 1)
val _ = check_coefficients "(- 1.5)" (~15, 10)
val _ = check_coefficients "(- 0.5)" (~5, 10)
val _ = check_coefficients "1/1" (1, 1)
val _ = check_coefficients "47/28" (47, 28)
val _ = check_coefficients "-47/28" (~47, 28)
val _ = check_coefficients "(- 47/28)" (~47, 28)
val _ = check_coefficients "0.05" (5, 100)
val _ = check_coefficients "1.05" (105, 100)
val _ = check_coefficients "0.005" (5, 1000)
val _ = check_coefficients "-0.5" (~5, 10)
val _ = check_coefficients "-1.5" (~15, 10)
val _ = check_coefficients "-0.05" (~5, 100)


›


(* Test alethe_replay_methods.ML *)
(* Important: The context can be different than if a step appears inside a proof! E.g., because
of subproofs. Any failure should be double checked carefully. Nonetheless, these regressions are useful
when changes are made to the reconstruction functions. 
Currently only supports indexes as args ^^ This is because the reconstruction of these rules had
some errors.
*)

ML‹
datatype token = None | Unfinished of string list * int | Finished of string list * string list
exception TOKEN of string

fun parse_token s [] = s |
  parse_token None ("("::cs) = parse_token (Unfinished(["("],1)) cs |
  parse_token None (" "::cs) = parse_token None cs |
  parse_token None (")"::cs) = Scan.fail cs |
  parse_token None cs = Finished (Scan.catch Scan.many (fn c => c <> " " andalso c <> ")") cs) |
  parse_token (Unfinished (s,i)) ("("::cs) = parse_token (Unfinished ("("::s,i+1)) cs |
  parse_token (Unfinished (_,0)) (")"::_) = raise TOKEN("too many closing parenthesis") |
  parse_token (Unfinished (s,1)) (")"::xs) = Finished(rev (")"::s),xs) |
  parse_token (Unfinished (s,i)) (")"::cs) = parse_token (Unfinished (")"::s,i-1)) cs |
  parse_token (Unfinished (s,i)) (c::cs) = parse_token (Unfinished (c::s,i)) cs |
  parse_token _ _ = raise TOKEN("error parsing token")

fun call_parse_token cs = parse_token (Unfinished ([],0)) cs |> (fn Finished(x,xs) => (x |> implode ,xs))

val scanWhiteSpace = Scan.many (curry (op =) " ")

fun tactic_args_parser ctxt cs =
   ((Scan.this_string "Declarations" |-- $$" " |-- scanWhiteSpace |-- $$"[" |-- scanWhiteSpace
     |-- Scan.repeat (call_parse_token --| scanWhiteSpace --| $$"," --| scanWhiteSpace)
     -- call_parse_token
     --| scanWhiteSpace --| $$"]"
   ) cs 
  |> fst
  |> (fn (xs,x) => x::xs) 
  |> map (Syntax.parse_term ctxt))




fun get_tac n ctxt prems args = 
let
  val ctxt =
    ctxt |> put_simpset (SMT_Replay.make_simpset ctxt [])
  val rule = CVC5_Replay_Methods.cvc5_rule_of n |> @{print}
  val rule_name = rule |> Alethe_Replay_Methods.string_of_alethe_rule
  val _ = @{print}("Found tactic", rule_name)
  val _ = @{print}("args", args  )

  (*FIXME: For some reason this function gets called twice... This definitely should not be necessary*)
  val dummys = Const ("Pure.prop", @{typ "prop ⇒ prop"}) $ (Const ("Pure.term", @{typ "prop ⇒ prop"}) $ Const ("Pure.dummy_pattern", @{typ "prop"}))

  val prems=prems
  val step_args=[]
  val context_args=[]
  (*arguments are only supported for some rules and are a little brittle*)
  (*maybe I should have parsed tokens, at the time I wrote this I only wanted to test one specific rule*)
  val args= (if member (op =) ["and_pos", "or_neg", "Not_Or", "and"] rule_name andalso Option.isSome args
            then SOME (Index (Option.valOf args |> Syntax.read_term ctxt |> HOLogic.dest_number |> snd))
            else if rule_name = "shuffle" andalso Option.isSome args
            then SOME (CommOp (Option.valOf args |> Syntax.read_term ctxt))
            else if rule_name = "la_generic" andalso Option.isSome args
            (*There has to be an int parser from a string out there...*)
            then 

let
val keyword_list = Keyword.empty_keywords |> Keyword.add_major_keywords [")","("]
 |> Keyword.add_major_keywords ["[","]"] |> Keyword.add_major_keywords [","]

(*TODO: there should be an optional in this for the last comma and can be made far nicer, had to get this working quick*)
val x = (Option.valOf args |> Token.explode keyword_list Position.none
        |> Parse.command_name "["  
        |-- 
 Scan.repeat (Parse.command_name "(" |-- Parse.int --| Parse.command_name "," -- Parse.int --| Parse.command_name ")"
 --| ( Parse.command_name ","))
--  (Parse.command_name "(" |-- Parse.int --| Parse.command_name "," -- Parse.int --| Parse.command_name ")")
 --| ( Parse.command_name "]")
) |> fst |> (fn (ys,z) => ys @ [z])

in 
SOME (Farkas_Coefficients x)
end
            else NONE)|> @{print}
  fun rule_tac ctxt t = CVC5_Replay_Methods.choose (Context.the_generic_context ()) rule ctxt prems step_args context_args t args
  fun term_to_thm t = rule_tac ctxt t

in
  (fn t => 
  if (t |> Thm.concl_of) = dummys
  then Seq.empty
  else
    let
      val thm2 = t |> Thm.concl_of |> (fn Const (_, _) $ x => x | x => x) |> term_to_thm 
    in
      resolve0_tac [thm2] 1 t
    end)
end

val parse_tactic_args : tactic_args parser = (fn ts => let val _ = @{print}("ts",ts) in (Index 0,ts) end)
fun test x = Parse.term (x|> @{print})
val _ =
 Theory.setup
 (Method.setup \<^binding>‹ctxt_tactic›
 (Scan.lift (Parse.string
             -- ( (Scan.optional (Scan.option Parse.string) NONE))) >>
   (fn (rule_name,args) => fn ctxt => fn prems => CONTEXT_TACTIC (get_tac rule_name ctxt prems args)))
 "testing tactics <name> ([<step_args>*]) ([<args>*])")
›


(* Rule 1: assume *)

lemma normalized_input_1:
  assumes "a"
  shows "a"
  using assms
  by (ctxt_tactic "__normalized_input")

lemma normalized_input_2:
  assumes "a ∧ (b ∨ c)"
  shows "a ∧ (b ∨ c)"
  using assms
  by (ctxt_tactic "__normalized_input")

lemma normalized_input_3:
  assumes "a ∧ a"
  shows "a ∧ a"
  using assms
  by (ctxt_tactic "__normalized_input")

lemma normalized_input_4:
  assumes "(∀a. a = (3::int))"
  shows "(∀a. a = (3::int))"
  using assms
  by (ctxt_tactic "__normalized_input")

lemma local_input_1:
  assumes "(∀a. a = (3::int))"
  shows "(∀a. a = (3::int))"
  using assms
  by (ctxt_tactic "__local_input")

lemma local_input_2:
  assumes "a ∧ (b ∨ c)"
  shows "a ∧ (b ∨ c)"
  using assms
  by (ctxt_tactic "__local_input")

lemma local_input_3:
  assumes "a ∧ a"
  shows "a ∧ a"
  using assms
  by (ctxt_tactic "__local_input")

lemma local_input_4:
  assumes "(∀a. a = (3::int))"
  shows "(∀a. a = (3::int))"
  using assms
  by (ctxt_tactic "__local_input")

(* Rule 2: hole *)

(* No checking necessary*)

(* Rule 3: true*)

lemma true_1: "True"
  by (ctxt_tactic "true")

(* Rule 4: false*)

lemma false_1: "¬False"
  by (ctxt_tactic "false_rule")

(* Rule 5: not_not*)

lemma not_not_1: "¬¬¬a ∨ a"
  by (ctxt_tactic "not_not")

lemma not_not_2: "¬¬¬¬a ∨ ¬a"
  by (ctxt_tactic "not_not")

lemma not_not_3: "¬¬¬(¬a ∨ b) ∨ (¬a ∨ b)"
  by (ctxt_tactic "not_not")

(* Rule 6 & 7: resolution and th_resolution*)

lemma resolution_1:
  assumes "a" "¬a"
  shows "False"
  using assms
  by (ctxt_tactic "resolution")

lemma resolution_2:
  assumes "a ∨ b" "¬a"
  shows "b"
  using assms
  by (ctxt_tactic "resolution")

lemma resolution_3:
  assumes "a ∨ b" "¬a ∨ c"
  shows "b ∨ c"
  using assms
  by (ctxt_tactic "resolution")


lemma
  assumes ‹¬ t1 ∨
    ¬ t2 ∨
    ¬ t3 ∨
    ¬ t4 ∨ ¬ t5 ∨ ¬ t6 ∨ ¬ t7 ∨ ¬ t8 ∨ ¬ t9 ∨ ¬ t10 ∨ ¬ t11 ∨ ¬ t12 ∨ ¬ t13 ∨ ¬ t14 ∨ ¬ t15 ∨
     ¬ t16 ∨ ¬ t17 ∨ ¬ t18 ∨ ¬ t19 ∨ ¬ t20 ∨ ¬ t21 ∨ ¬ t22 ∨ ¬ t23 ∨ ¬ t24 ∨ ¬ t25 ∨ t26›
    ‹¬ t27 ∨ t1›
    ‹¬ t27 ∨ t2›
    ‹¬ t27 ∨ t3›
    ‹¬ t27 ∨ t4›
    ‹¬ t27 ∨ t5›
    ‹¬ t27 ∨ t6›
    ‹¬ t27 ∨ t7›
    ‹¬ t27 ∨ t8›
    ‹¬ t27 ∨ t9›
    ‹¬ t27 ∨ t10›
    ‹¬ t27 ∨ t11›
    ‹¬ t27 ∨ t12›
    ‹¬ t27 ∨ t13›
    ‹¬ t27 ∨ t14›
    ‹¬ t27 ∨ t15›
    ‹¬ t27 ∨ t16›
    ‹¬ t27 ∨ t17›
    ‹¬ t27 ∨ t18›
    ‹¬ t27 ∨ t19›
    ‹¬ t27 ∨ t20›
    ‹¬ t27 ∨ t21›
    ‹¬ t27 ∨ t22›
    ‹¬ t27 ∨ t23›
    ‹¬ t27 ∨ t24›
    ‹¬ t27 ∨ t25›
  shows ‹t26 ∨
    ¬ t27 ∨
    ¬ t27 ∨
    ¬ t27 ∨
    ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27 ∨ ¬ t27›
  using assms
  by (ctxt_tactic "resolution")

(* Rule 8: tautology *)

lemma tautology_1:
  assumes "a ∨ b ∨ ¬a ∨ c"
  shows "True"
  using assms
  by (ctxt_tactic "tautology")

(* Rule 9: contraction *)

lemma contraction_1:
  assumes "a ∨ b"
  shows "a ∨ b"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_2:
  assumes "a ∨ a"
  shows "a"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_3:
  assumes "a ∨ b ∨ a ∨ c"
  shows "a ∨ b ∨ c"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_4:
  assumes "a ∨ b ∨ a ∨ b"
  shows "a ∨ b"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_5:
  assumes "a ∨ (b ⟶ c) ∨ (b ⟶ c) ∨ b"
  shows "a ∨ (b ⟶ c) ∨ b"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_6:
  assumes "a ∨ (b ∨ c) ∨ (b ∨ c) ∨ b"
  shows "a ∨ (b ∨ c) ∨ b"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_7:
  assumes "(b ∨ c) ∨ a ∨ (b ∨ c)"
  shows "a ∨ (b ∨ c)"
  using assms
  by (ctxt_tactic "contraction")

lemma contraction_8:
  assumes "((¬ y3 ∨ ¬ y689) ∨ ¬ ¬ y689) ∨ (¬ y3 ∨ ¬ y689) ∨ ¬ ¬ y689"
  shows "(¬ y3 ∨ ¬ y689) ∨ ¬ ¬ y689"
  using assms
  by (ctxt_tactic "contraction")

context
  fixes P :: ‹nat ⇒ bool›
begin
(*cvc5 sometimes produces extremely large goals (6000 lines of Isabelle terms if you print
it as a lemma), so here is an ML version to be able to measure time.*)
ML ‹
let
  fun build_term n = 
    if n = 0 then @{term ‹P 0›}
    else HOLogic.mk_disj (@{term ‹P›} $ HOLogic.mk_nat (n),  build_term (n-1))
  fun build_term2 n = 
    if n = 0 then @{term ‹P 0›}
    else HOLogic.mk_disj (build_term2 (n-1), 
       HOLogic.mk_disj (@{term ‹P›} $ HOLogic.mk_nat (n), build_term (n-1)))
  val ctxt = @{context}
  fun measure_time ctxt n =
    let
    val ct = (Thm.cterm_of ctxt) (build_term2 n) |> HOLogic.mk_judgment
    val (prems, ctxt') = Assumption.add_assumes [ct] ctxt
    val start = Timing.start ()
    val thm = Alethe_Replay_Methods.contraction ctxt' prems (@{term Trueprop} $ build_term n)
    val total = Time.toMilliseconds (#elapsed (Timing.result start))
    in
     (thm, total)
    end
in
   map (measure_time ctxt) [10,20,30,50,60]
end
›
end

(* Rule 11: la_generic *)

declare[[smt_debug_arith_verit]]
declare[[show_types=false,show_hyps=false]]
declare[[ML_print_depth=1000]]

lemma la_generic_1:
"
¬ - 1 * ((x8::int) + - 1 * y8 + x1 + - 1 * y1) ≤ - 1 * 1 ∨
¬ x8 + - 1 * y8 + - 1 * x2 + y2 + x1 + - 1 * y1 + - 1 * x0 + y0 ≤ 0 ∨
¬ x2 + - 1 * y2 + x0 + - 1 * y0 < 1 ∨
- 1 * (x8 + - 1 * y8 + x1 + - 1 * y1) + 
  (x8 + - 1 * y8 + - 1 * x2 + y2 + x1 + - 1 * y1 + - 1 * x0 + y0) +
  (x2 + - 1 * y2 + x0 + - 1 * y0)
  < - 1 * 1 + 0 + 1 "
  by (ctxt_tactic "la_generic" "[(1,1),(1,1),(1,1),(1,1)]")


lemma la_generic_2:
  fixes x8::int
  shows 
"
¬ - x1 + y1 - x8 + y8 ≤ - 1 ∨
¬   x1 - y1 + x8 - y8 - x0 + y0 - x2 + y2 ≤ 0 ∨
¬                       x0 - y0 + x2 - y2 < 1 ∨
0 < 0 "
  by (ctxt_tactic "la_generic" "[(1,1),(1,1),(1,1),(1,1)]")

(* The original problem had t1,t2 :: real, but int also had the same issue *)
lemma la_generic_3:
  fixes t1::int and t2::int
  shows "(t1 ≠ -1) ∨ (t2 ≠ (-t2)) ∨ ((-t2) ≠ (-t1))"
  by (ctxt_tactic "la_generic" "[(-2,1),(1,1),(2,1)]")

(* Rule 12: lia_generic *)

lemma lia_generic_1:
  shows "¬(3*(x::int) = 9) ∨ (x ≥ 3)"
  by (ctxt_tactic "lia_generic")

(* Rule 13: la_disequality *)

lemma la_disequality_1: "(a::int) = b ∨ ¬ (a::int) ≤ b ∨ ¬ b ≤ (a::int)"
  by (ctxt_tactic "la_disequality")

lemma la_disequality_2: "(1::int) = (5-4) ∨ ¬ (1::int) ≤ (5-4) ∨ ¬ (5-4) ≤ (1::int)"
  by (ctxt_tactic "la_disequality")

lemma la_disequality_3: "(2::int) = (7-2) ∨ ¬ (2::int) ≤ (7-2) ∨ ¬ (7-2) ≤ (2::int)"
  by (ctxt_tactic "la_disequality")

lemma la_disequality_4: "(2::int) = (7-6) ∨ ¬ (2::int) ≤ (7-6) ∨ ¬ (7-6) ≤ (2::int)"
  by (ctxt_tactic "la_disequality")


(* Rule 14: la_totality *)

lemma la_totality_1: "(a::int) ≤ b ∨ b ≤ a"
  by (ctxt_tactic "la_totality")

lemma la_totality_2: "((2::int) - 6) ≤ (3 + 4) ∨ (3 + 4)  ≤ ((2::int) - 6)"
  by (ctxt_tactic "la_totality")


(* Rule 15: la_tautology *)

lemma la_tautology_form1_1: "¬((1::int) = 2)"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form1_2: "((2::int) < 5)"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form1_3: "((14::int) ≥ 6)"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form1_4: "((14::int) ≥ (6-3+1))"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form1_5: "¬((-14::int) ≥ -(6-3+1))"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form2_1: "((a::int) ≤ 11) ∨ ¬(a ≤ 11)"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form2_2: "(a::int) ≤ 11 ∨ ¬(a ≤ (66 - 55))"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form2_3: "¬(((5::int) + 4) ≤ 11) ∨ ¬(((5::int) + 4) ≥ 11)"
  by (ctxt_tactic "la_tautology")

lemma la_tautology_form2_4: "¬(((5::int) + 4) ≤ 11) ∨ ¬(((5::int) + 4) ≥ 25)"
  by (ctxt_tactic "la_tautology")


(* Rule 16: la_mult_pos*)

lemma la_mult_pos_1: "(0::int) < 3 ∧ (A::int) < 0 ⟶ 3 * A < 3 * 0 "
  by (ctxt_tactic "la_mult_pos")

lemma la_mult_pos_2: "(0::int) < 3 ∧ (-3::int) < 0 ⟶ (3::int) * (-3) < 3 * 0"
  by (ctxt_tactic "la_mult_pos")

lemma la_mult_pos_3: "(0::int) < 5 ∧ ¬((-3::int) = -77) ⟶ ¬((5::int) * (-3) = 5 * -77)"
  by (ctxt_tactic "la_mult_pos")


(* Rule 23: trans *)                              

lemma trans_1:
  assumes "a = a"
  shows  "a = a"
  using assms
  by (ctxt_tactic "trans")

lemma trans_2:
  assumes "a = a" "a = b"
  shows  "a = b"
  using assms
  by (ctxt_tactic "trans")

lemma trans_3:
  assumes "(a = f a)" "(f a = b)"
  shows  "a = b"
  using assms
  by (ctxt_tactic "trans")

lemma trans_4:
  assumes "(a = f a)" "(f a = b)" "(b = a)"
  shows  "a = a"
  using assms
  by (ctxt_tactic "trans")

lemma trans_5:
assumes "f a b = f a (g b)"
        "f a (g b) = f a b"
        "f a b = True"
shows   "f a b = True"
  using assms
  by (ctxt_tactic "trans")

(* Rule 24: cong *)

lemma cong_1: 
  assumes "(a = a)"
  shows "(a = a)"
  using assms
  by (ctxt_tactic "eq_congruent")

lemma cong_2:
  assumes "(a = a)" and "(a = b)"
  shows "(f a a) = (f a b)"
  using assms
  by (ctxt_tactic "cong")

lemma cong_3:
  assumes "(3 = 2 + (1::int))" and "(c = g b)"
  shows "((3 + c) = ((2 + (1::int)) + g b))"
  using assms
  by (ctxt_tactic "cong")

lemma cong_4:
  assumes "x = False"
  shows "alethe_id (λa b. a = b) x = alethe_id (λa b. a = b) False"
  using assms
  by (ctxt_tactic "cong")

lemma cong_5:
  assumes "alethe_id (λa. f a x) = alethe_id (λa. f a y)" and "s = t"
  shows "alethe_id (λa. f a x) s = alethe_id (λa. f a y) t"
  using assms
  by (ctxt_tactic "cong")

(* Rule 25: eq_reflexive *)

lemma eq_reflexive_1: "a = a"
  by (ctxt_tactic "eq_reflexive")

lemma eq_reflexive_2: "3 = (3::int)"
  by (ctxt_tactic "eq_reflexive")

lemma eq_reflexive_3: "(a = b) = (a = b)"
  by (ctxt_tactic "eq_reflexive")

(* Rule 26: eq_transitive *)

lemma eq_transitive_1: "¬ (a = a) ∨ (a = a)"
  by (ctxt_tactic "eq_transitive")

lemma eq_transitive_2: "¬ (a = a) ∨ ¬(a = b) ∨ (a = b)"
  by (ctxt_tactic "eq_transitive")

lemma eq_transitive_3: "¬ (a = f a) ∨ ¬(f a = b) ∨ (a = b)"
  by (ctxt_tactic "eq_transitive")

lemma eq_transitive_4: "¬ (a = f a) ∨ ¬(f a = b) ∨ ¬(f a = a) ∨ (a = a)"
  by (ctxt_tactic "eq_transitive")

(* Rule 27: eq_congruent *)

lemma eq_congruent_1: "¬ (a = a) ∨ (a = a)"
  by (ctxt_tactic "eq_congruent")

lemma eq_congruent_2: "¬ (a = a) ∨ ¬(a = b) ∨ (f a a = f a b)"
  by (ctxt_tactic "eq_congruent")

lemma eq_congruent_3: "¬ (3 = 2 + (1::int)) ∨ ¬(c = g b) ∨ ((3 + c) = ((2 + (1::int)) + g b))"
  by (ctxt_tactic "eq_congruent")

lemma eq_congruent_5:
  shows "¬(3 = 2 + (1::int)) ∨ ¬c = g b ∨ ((3 + c) = ((2 + (1::int)) + g b))"
  by (ctxt_tactic "eq_congruent")


(* Rule 28: eq_congruent_pred *)

lemma eq_congruent_pred_1: "¬ (a = a) ∨ (a = a)"
  by (ctxt_tactic "eq_congruent_pred")

lemma eq_congruent_pred_2: "¬ (a = a) ∨ ¬(a = b) ∨ (P a a = P a b)"
  by (ctxt_tactic "eq_congruent_pred")

(* Rule 29: qnt_cnf *)

lemma qnt_cnf_1: "¬ (∀x1::'a. ¬((x1 = 1) ∨ (x1 = 2))) ∨ (∀x1::'a::{numeral}. (¬(x1 = 1) ∧ ¬(x1 = 2)))"
 by (ctxt_tactic "qnt_cnf")

lemma qnt_cnf_2: ‹¬ (∀veriT_vr1::'a. ¬ (P::bool ⇒ 'a ⇒ bool) False veriT_vr1 ∧ P True veriT_vr1) ∨
         (∀veriT_vr1::'a. P True veriT_vr1) ›
 by (ctxt_tactic "qnt_cnf")

lemma qnt_cnf_3:
  fixes trans
  shows
        "¬ (∀(veriT_vr756::int) veriT_vr757 veriT_vr758 (veriT_vr759::int) (veriT_vr760::int) veriT_vr761 veriT_vr762.
                (fun_app (t veriT_vr756 veriT_vr757 veriT_vr758) (trans veriT_vr759 veriT_vr760 veriT_vr761 veriT_vr762) ⟶
                 (∃veriT_vr763.
                     membera veriT_vr763 veriT_vr756 ∧
                     membera veriT_vr763 (seta (userIDs veriT_vr762)) ∧
                     memberb veriT_vr757 (setb (fun_appv (outerPostIDs veriT_vr762) veriT_vr758)) ∧
                     (veriT_vr763 = admin veriT_vr762 ∨
                      memberh (pairb veriT_vr758 (fun_appn (fun_appz (outerOwner veriT_vr762) veriT_vr758) veriT_vr757)) (setf (fun_appaa (recvOuterFriendIDs veriT_vr762) veriT_vr763)) ∨
                      vsb
                       (literal False False False False True True True
                         (literal True False True False True True True
                           (literal False True False False False True True
                             (literal False False True True False True True (literal True False False True False True True (literal True True False False False True True zero)))))) =
                      fun_appl (fun_appy (outerVis veriT_vr762) veriT_vr758) veriT_vr757))) ∧
                (¬ (∀veriT_vr764.
                        ¬ (membera veriT_vr764 veriT_vr756 ∧
                            membera veriT_vr764 (seta (userIDs veriT_vr762)) ∧
                            memberb veriT_vr757 (setb (fun_appv (outerPostIDs veriT_vr762) veriT_vr758)) ∧
                            (admin veriT_vr762 = veriT_vr764 ∨
                             memberh (pairb veriT_vr758 (fun_appn (fun_appz (outerOwner veriT_vr762) veriT_vr758) veriT_vr757)) (setf (fun_appaa (recvOuterFriendIDs veriT_vr762) veriT_vr764)) ∨
                             vsb
                              (literal False False False False True True True
                                (literal True False True False True True True
                                  (literal False True False False False True True
                                    (literal False False True True False True True (literal True False False True False True True (literal True True False False False True True zero)))))) =
                             fun_appl (fun_appy (outerVis veriT_vr762) veriT_vr758) veriT_vr757))) ⟶
                 fun_app (t veriT_vr756 veriT_vr757 veriT_vr758) (trans veriT_vr759 veriT_vr760 veriT_vr761 veriT_vr762))) ∨
         (∀veriT_vr756 veriT_vr757 veriT_vr758 veriT_vr759 (veriT_vr760::int) veriT_vr761 veriT_vr762 veriT_vr764.
             ¬ membera veriT_vr764 veriT_vr756 ∨
             ¬ membera veriT_vr764 (seta (userIDs veriT_vr762)) ∨
             ¬ memberb veriT_vr757 (setb (fun_appv (outerPostIDs veriT_vr762) veriT_vr758)) ∨
             vsb
              (literal False False False False True True True
                (literal True False True False True True True
                  (literal False True False False False True True
                    (literal False False True True False True True (literal True False False True False True True (literal True True False False False True True zero)))))) ≠
             fun_appl (fun_appy (outerVis veriT_vr762) veriT_vr758) veriT_vr757 ∨
             fun_app (t veriT_vr756 veriT_vr757 veriT_vr758) (trans veriT_vr759 veriT_vr760 veriT_vr761 veriT_vr762))
"
  by (ctxt_tactic "qnt_cnf")

lemma qnt_cnf_4: ‹ ¬ (∀(veriT_vr13::'a_topoly::type) veriT_vr14::'a::type option set.
                ((Alexandroff_open::'a_topoly::type ⇒ 'a::type option set ⇒ bool) veriT_vr13 veriT_vr14 ⟶
                 (∃veriT_vr15::'a::type set.
                     veriT_vr14 = Some ` veriT_vr15 ∧ (openin::'a_topoly::type ⇒ 'a::type set ⇒ bool) veriT_vr13 veriT_vr15 ∨
                     veriT_vr14 = insert None (Some ` ((topspace::'a_topoly::type ⇒ 'a::type set) veriT_vr13 - veriT_vr15)) ∧
                     (compactin::'a_topoly::type ⇒ 'a::type set ⇒ bool) veriT_vr13 veriT_vr15 ∧ (closedin::'a_topoly::type ⇒ 'a::type set ⇒ bool) veriT_vr13 veriT_vr15)) ∧
                (¬ (∀veriT_vr16::'a::type set.
                        ¬ (veriT_vr14 = Some ` veriT_vr16 ∧ openin veriT_vr13 veriT_vr16 ∨
                            veriT_vr14 = insert None (Some ` (topspace veriT_vr13 - veriT_vr16)) ∧ compactin veriT_vr13 veriT_vr16 ∧ closedin veriT_vr13 veriT_vr16)) ⟶
                 Alexandroff_open veriT_vr13 veriT_vr14)) ∨
         (∀(veriT_vr13::'a_topoly::type) (veriT_vr14::'a::type option set) veriT_vr16::'a::type set.
             veriT_vr14 ≠ insert None (Some ` (topspace veriT_vr13 - veriT_vr16)) ∨
             ¬ compactin veriT_vr13 veriT_vr16 ∨ ¬ closedin veriT_vr13 veriT_vr16 ∨ Alexandroff_open veriT_vr13 veriT_vr14) ›
  by (ctxt_tactic "qnt_cnf")

lemma qnt_cnf_5:
  fixes ACIDZ (infix ‹~› 64)
  shows
  ‹¬ (∀(veriT_vr58::'a_rexp) veriT_vr59::'a_rexp.
        (veriT_vr58 ~ veriT_vr59 ⟶
                 (∃(veriT_vr60::'a_rexp) (veriT_vr61::'a_rexp) veriT_vr62::'a_rexp.
                     veriT_vr58 = Alt (Alt veriT_vr60 veriT_vr61) veriT_vr62 ∧ veriT_vr59 = Alt veriT_vr60 (Alt veriT_vr61 veriT_vr62)) ∨
                 (∃(veriT_vr63::'a_rexp) (veriT_vr64::'a_rexp) veriT_vr65::'a_rexp.
                     veriT_vr58 = Alt veriT_vr63 (Alt veriT_vr64 veriT_vr65) ∧ veriT_vr59 = Alt (Alt veriT_vr63 veriT_vr64) veriT_vr65) ∨
                 (∃(veriT_vr66::'a_rexp) veriT_vr67::'a_rexp. veriT_vr58 = Alt veriT_vr66 veriT_vr67 ∧ veriT_vr59 = Alt veriT_vr67 veriT_vr66) ∨
                 veriT_vr59 = Alt veriT_vr58 veriT_vr58 ∨
                 (∃veriT_vr68::'a_rexp. veriT_vr59 = elim_zeros veriT_vr68 ∧ veriT_vr58 ~ veriT_vr68) ∨
                 (∃(veriT_vr69::'a_rexp) veriT_vr70::'a_rexp. veriT_vr58 = Conc veriT_vr69 veriT_vr70 ∧ veriT_vr59 = distribute veriT_vr70 veriT_vr69) ∨
                 veriT_vr58 = veriT_vr59 ∨
                 (∃(veriT_vr71::'a_rexp) (veriT_vr72::'a_rexp) (veriT_vr73::'a_rexp) veriT_vr74::'a_rexp.
                     veriT_vr58 = Alt veriT_vr71 veriT_vr73 ∧ veriT_vr59 = Alt veriT_vr72 veriT_vr74 ∧ veriT_vr71 ~ veriT_vr72 ∧ veriT_vr73 ~ veriT_vr74) ∨
                 (∃(veriT_vr75::'a_rexp) (veriT_vr76::'a_rexp) veriT_vr77::'a_rexp.
                     veriT_vr58 = Conc veriT_vr75 veriT_vr77 ∧ veriT_vr59 = Conc veriT_vr76 veriT_vr77 ∧ veriT_vr75 ~ veriT_vr76)) ∧
        (¬ (∀(veriT_vr78::'a_rexp) (veriT_vr79::'a_rexp) veriT_vr80::'a_rexp.
                        ¬ (veriT_vr58 = Alt (Alt veriT_vr78 veriT_vr79) veriT_vr80 ∧ veriT_vr59 = Alt veriT_vr78 (Alt veriT_vr79 veriT_vr80))) ∨
                 ¬ (∀(veriT_vr81::'a_rexp) (veriT_vr82::'a_rexp) veriT_vr83::'a_rexp.
                        ¬ (veriT_vr58 = Alt veriT_vr81 (Alt veriT_vr82 veriT_vr83) ∧ veriT_vr59 = Alt (Alt veriT_vr81 veriT_vr82) veriT_vr83)) ∨
                 ¬ (∀(veriT_vr84::'a_rexp) veriT_vr85::'a_rexp. ¬ (veriT_vr58 = Alt veriT_vr84 veriT_vr85 ∧ veriT_vr59 = Alt veriT_vr85 veriT_vr84)) ∨
                 veriT_vr59 = Alt veriT_vr58 veriT_vr58 ∨
                 ¬ (∀veriT_vr86::'a_rexp. ¬ (veriT_vr59 = elim_zeros veriT_vr86 ∧ veriT_vr58 ~ veriT_vr86)) ∨
                 ¬ (∀(veriT_vr87::'a_rexp) veriT_vr88::'a_rexp. ¬ (veriT_vr58 = Conc veriT_vr87 veriT_vr88 ∧ veriT_vr59 = distribute veriT_vr88 veriT_vr87)) ∨
                 veriT_vr58 = veriT_vr59 ∨
                 ¬ (∀(veriT_vr89::'a_rexp) (veriT_vr90::'a_rexp) (veriT_vr91::'a_rexp) veriT_vr92::'a_rexp.
                        ¬ (veriT_vr58 = Alt veriT_vr89 veriT_vr91 ∧ veriT_vr59 = Alt veriT_vr90 veriT_vr92 ∧ veriT_vr89 ~ veriT_vr90 ∧ veriT_vr91 ~ veriT_vr92)) ∨
                 ¬ (∀(veriT_vr93::'a_rexp) (veriT_vr94::'a_rexp) veriT_vr95::'a_rexp.
                        ¬ (veriT_vr58 = Conc veriT_vr93 veriT_vr95 ∧ veriT_vr59 = Conc veriT_vr94 veriT_vr95 ∧ veriT_vr93 ~ veriT_vr94)) ⟶
                 veriT_vr58 ~ veriT_vr59)) ∨
    (∀(veriT_vr58::'a_rexp) veriT_vr59::'a_rexp. veriT_vr58 ≠ veriT_vr59 ∨ veriT_vr58 ~ veriT_vr59)›
  supply [[show_types]]
  by (ctxt_tactic "qnt_cnf")

lemma
  fixes scaleR :: "'real ⇒ 'a :: {comm_monoid_add,inverse,times,zero,ord} ⇒ 'a" (infixr ‹*⇩R› 75)
  shows ‹¬ (∀veriT_vr37.
                veriT_vr37 ∈ space M ⟶
                (∑uua∈f ` space M. indicat_real (f -` {uua} ∩ space M) veriT_vr37 *⇩R uua) = f veriT_vr37) ∨
         (∀veriT_vr37.
             veriT_vr37 ∉ space M ∨
             (∑uua∈f ` space M. indicat_real (f -` {uua} ∩ space M) veriT_vr37 *⇩R uua) = f veriT_vr37) ›
  by (ctxt_tactic "qnt_cnf")

lemma ‹¬ (∀veriT_vr7 veriT_vr8 veriT_vr9 :: 'a.
                (veriT_vr7 / veriT_vr8 < veriT_vr9) =
                (if 0 < veriT_vr8 then veriT_vr7 < veriT_vr9 * veriT_vr8
                 else if veriT_vr8 < 0 then veriT_vr9 * veriT_vr8 < veriT_vr7 else 0 < veriT_vr9)) ∨
         (∀veriT_vr7 veriT_vr8 veriT_vr9 :: 'a:: {comm_monoid_add,inverse,times,zero,ord}.
             ¬ veriT_vr7 / veriT_vr8 < veriT_vr9 ∨ ¬ 0 < veriT_vr8 ∨ veriT_vr7 < veriT_vr9 * veriT_vr8)›
  by (ctxt_tactic "qnt_cnf")

lemma
  fixes Cons :: ‹'a :: {zero} ⇒ 'alist ⇒ 'alist› (infix ‹#› 70) and Nil :: 'alist
  shows ‹¬ (∀veriT_vr18 veriT_vr19. poly Nil ≠ poly (veriT_vr18 # veriT_vr19) ∨ 0 = veriT_vr18 ∧ poly Nil = poly veriT_vr19)
    ∨ (∀veriT_vr18. 0 = veriT_vr18 ∨ (∀veriT_vr19. poly Nil ≠ poly (veriT_vr18 # veriT_vr19)))›
  supply [[show_types]] by (ctxt_tactic "qnt_cnf")

lemma
  fixes Sum :: "['a,'a,'a,'a,'a,'a] ⇒ bool" ("Sum _ _ _ _ _ _" [99,99,99,99,99,99] 50) 
  shows
    ‹¬ (∀veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 veriT_vr86 veriT_vr87 veriT_vr88.
                Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 ∧
                Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr84 veriT_vr86 veriT_vr87 ⟶
                (Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr87 veriT_vr88) =
                (Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr85 veriT_vr86 veriT_vr88)) ∨
         (∀veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 veriT_vr86 veriT_vr87 veriT_vr88.
             ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 ∨
             ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr84 veriT_vr86 veriT_vr87 ∨
             ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr85 veriT_vr86 veriT_vr88 ∨
             Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr87 veriT_vr88) ›
  by (ctxt_tactic "qnt_cnf")

lemma 
  fixes Sum :: "['a,'a,'a,'a,'a,'a] ⇒ bool" ("Sum _ _ _ _ _ _" [99,99,99,99,99,99] 50) and
        Opp :: "['a,'a,'a,'a,'a] ⇒ bool" ("Opp _ _ _ _ _" [99,99,99,99,99] 50) and
        Diff :: "['a,'a,'a,'a,'a,'a] ⇒ bool" ("Diff _ _ _ _ _ _" [99,99,99,99,99,99] 50)
  shows ‹¬ (∀veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 veriT_vr86 veriT_vr87 veriT_vr88.
            Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 ∧
            Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr84 veriT_vr86 veriT_vr87 ⟶
            (Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr87 veriT_vr88) =
            (Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr85 veriT_vr86 veriT_vr88)) ∨
     (∀veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 veriT_vr86 veriT_vr87 veriT_vr88.
         ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr84 veriT_vr85 ∨
         ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr84 veriT_vr86 veriT_vr87 ∨
         ¬ Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr85 veriT_vr86 veriT_vr88 ∨
         Sum veriT_vr80 veriT_vr81 veriT_vr82 veriT_vr83 veriT_vr87 veriT_vr88)›
  by (ctxt_tactic "qnt_cnf")

locale _ =
  fixes order :: "'energy ⇒ 'energy ⇒ bool"  (infix ‹e≤› 80) and
        energies :: "'energy set"
begin

abbreviation "incomparable P ≡ λx y. ¬ P x y ∧ ¬ P y x"

lemma
  fixes P :: ‹('position ⇒ 'energy set) set› and veriT_vr29
  defines ‹Delta ≡ λveriT_vr29. {uua::'energy. ∃F::'position ⇒ 'energy set. F ∈ P ∧ uua ∈ F veriT_vr29}›
  shows ‹ ¬ (∀(veriT_vr29::'position) veriT_vr30::'energy.
                (veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀x::'energy. x ∈ Delta veriT_vr29 ∧ veriT_vr30 ≠ x ⟶ ¬ x e≤ veriT_vr30) ⟶
                 veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr31::'energy. veriT_vr31 ∈ Delta veriT_vr29 ∧ veriT_vr30 ≠ veriT_vr31 ⟶ ¬ veriT_vr31 e≤ veriT_vr30)) ∧
                (veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr32::'energy. veriT_vr32 ∈ Delta veriT_vr29 ∧ veriT_vr30 ≠ veriT_vr32 ⟶ ¬ veriT_vr32 e≤ veriT_vr30) ⟶
                 veriT_vr30 ∈ Delta veriT_vr29 ∧ (∀x::'energy. x ∈ Delta veriT_vr29 ∧ veriT_vr30 ≠ x ⟶ ¬ x e≤ veriT_vr30))) ∨
         (∀(veriT_vr29::'position) (veriT_vr30::'energy) veriT_vr31::'energy.
             ¬ (veriT_vr30 ∈ Delta veriT_vr29 ∧ (∀x::'energy. x ∈ Delta veriT_vr29 ∧ veriT_vr30 ≠ x ⟶ ¬ x e≤ veriT_vr30)) ∨
             veriT_vr31 ∉ Delta veriT_vr29 ∨ veriT_vr30 = veriT_vr31 ∨ ¬ veriT_vr31 e≤ veriT_vr30)›
  by (ctxt_tactic "qnt_cnf")

lemma
  fixes P :: ‹('position ⇒ 'energy set) set› and veriT_vr29
  defines ‹Delta ≡ λveriT_vr29. {uua::'energy. ∃F::'position ⇒ 'energy set. F ∈ P ∧ uua ∈ F veriT_vr29}›
  shows ‹ ¬ (∀(veriT_vr29::'position) veriT_vr30::'energy.
                (alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧
                 (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30)) ⟶
                 veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr31::'energy. alethe_Box (veriT_vr31 ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = veriT_vr31) ⟶ ¬ alethe_Box (veriT_vr31 e≤ veriT_vr30))) ∧
                (veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr32::'energy. alethe_Box (veriT_vr32 ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = veriT_vr32) ⟶ ¬ alethe_Box (veriT_vr32 e≤ veriT_vr30)) ⟶
                 alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧ (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30)))) ∨
         (∀(veriT_vr29::'position) (veriT_vr30::'energy) veriT_vr31::'energy.
             ¬ (alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧ (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30))) ∨
             ¬alethe_Box (veriT_vr31 ∈ Delta veriT_vr29) ∨ alethe_Box (veriT_vr30 = veriT_vr31) ∨ ¬ alethe_Box (veriT_vr31 e≤ veriT_vr30))›
  by (ctxt_tactic "qnt_cnf")

context
  fixes P :: ‹('position ⇒ 'energy set) set› and veriT_vr29 :: 'position
begin

abbreviation  ‹Delta ≡ λveriT_vr29. {uua::'energy. ∃F::'position ⇒ 'energy set. F ∈ P ∧ uua ∈ F veriT_vr29}›
lemma
  shows ‹ ¬ (∀(veriT_vr29::'position) veriT_vr30::'energy.
                (alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧
                 (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30)) ⟶
                 veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr31::'energy. alethe_Box (veriT_vr31 ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = veriT_vr31) ⟶ ¬ alethe_Box (veriT_vr31 e≤ veriT_vr30))) ∧
                (veriT_vr30 ∈ Delta veriT_vr29 ∧
                 (∀veriT_vr32::'energy. alethe_Box (veriT_vr32 ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = veriT_vr32) ⟶ ¬ alethe_Box (veriT_vr32 e≤ veriT_vr30)) ⟶
                 alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧ (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30)))) ∨
         (∀(veriT_vr29::'position) (veriT_vr30::'energy) veriT_vr31::'energy.
             ¬ (alethe_Box (veriT_vr30 ∈ Delta veriT_vr29) ∧ (∀x::'energy. alethe_Box (x ∈ Delta veriT_vr29) ∧ ¬alethe_Box (veriT_vr30 = x) ⟶ ¬ alethe_Box (x e≤ veriT_vr30))) ∨
             ¬alethe_Box (veriT_vr31 ∈ Delta veriT_vr29) ∨ alethe_Box (veriT_vr30 = veriT_vr31) ∨ ¬ alethe_Box (veriT_vr31 e≤ veriT_vr30))›
  by (ctxt_tactic "qnt_cnf")

lemma ‹  ¬ (∀(veriT_vr34::('a ⇒ bool) ⇒ bool) veriT_vr35::'a.
                (∄x::'a ⇒ bool. veriT_vr34 x ∧ x veriT_vr35) ∧
                ¬ (∀veriT_vr36::'a ⇒ bool.
                       ¬ (¬ (∀veriT_vr37::'a ⇒ bool. ¬ (veriT_vr34 veriT_vr37 ∧ veriT_vr36 = (φ::('a ⇒ bool) ⇒ 'a ⇒ bool) veriT_vr37)) ∧ veriT_vr36 veriT_vr35)) ⟶
                φ (λuua::'a. ∃x::'a ⇒ bool. veriT_vr34 x ∧ x uua) veriT_vr35) ∨
         (∀(veriT_vr34::('a ⇒ bool) ⇒ bool) (veriT_vr35::'a) (veriT_vr36::'a ⇒ bool) veriT_vr37::'a ⇒ bool.
             (∃x::'a ⇒ bool. veriT_vr34 x ∧ x veriT_vr35) ∨
             ¬ veriT_vr34 veriT_vr37 ∨ veriT_vr36 ≠ φ veriT_vr37 ∨ ¬ veriT_vr36 veriT_vr35 ∨ φ (λuua::'a. ∃x::'a ⇒ bool. veriT_vr34 x ∧ x uua) veriT_vr35)  ›
  by (ctxt_tactic "qnt_cnf")


lemma ‹¬ (∀veriT_vr13 veriT_vr14 veriT_vr15.
           inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) =
           (if 0 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15
            else 5 = veriT_vr14 ∧ inv_tm_skip_first_arg_len_eq_1_s5 veriT_vr13 veriT_vr15)) ∨
    (∀veriT_vr13 veriT_vr14 veriT_vr15.
        ¬ inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) ∨
        0 ≠ veriT_vr14 ∨ inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15) ›
  by (ctxt_tactic "qnt_cnf")

lemma ‹¬ (∀veriT_vr13 veriT_vr14 veriT_vr15.
           inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) =
           (if 0 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15
            else if 1 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s1 veriT_vr13 veriT_vr15
                 else if 2 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s2 veriT_vr13 veriT_vr15
                      else 5 = veriT_vr14 ∧ inv_tm_skip_first_arg_len_eq_1_s5 veriT_vr13 veriT_vr15)) ∨
    (∀veriT_vr13 veriT_vr14 veriT_vr15.
        ¬ inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) ∨
        0 ≠ veriT_vr14 ∨ inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15) ›
  by (ctxt_tactic "qnt_cnf")


lemma ‹¬ (∀veriT_vr13 veriT_vr14 veriT_vr15.
           inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) =
           (if 0 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15
            else if 1 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s1 veriT_vr13 veriT_vr15
                 else if 2 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s2 veriT_vr13 veriT_vr15
                      else if 3 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s3 veriT_vr13 veriT_vr15
                           else 5 = veriT_vr14 ∧ inv_tm_skip_first_arg_len_eq_1_s5 veriT_vr13 veriT_vr15)) ∨
    (∀veriT_vr13 veriT_vr14 veriT_vr15.
        ¬ inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) ∨
        0 ≠ veriT_vr14 ∨ inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15) ›
  by (ctxt_tactic "qnt_cnf")

lemma ‹¬ (∀veriT_vr13 veriT_vr14 veriT_vr15.
           inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) =
           (if 0 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15
            else if 1 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s1 veriT_vr13 veriT_vr15
                 else if 2 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s2 veriT_vr13 veriT_vr15
                      else if 3 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s3 veriT_vr13 veriT_vr15
                           else if 4 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s4 veriT_vr13 veriT_vr15
                                else 5 = veriT_vr14 ∧ inv_tm_skip_first_arg_len_eq_1_s5 veriT_vr13 veriT_vr15)) ∨
    (∀veriT_vr13 veriT_vr14 veriT_vr15.
        ¬ inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) ∨
        0 ≠ veriT_vr14 ∨ inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15) ›
  by (ctxt_tactic "qnt_cnf")

typedef✐‹tag important› 'a topology = "{L::('a set) ⇒ bool. True}"
  morphisms "openin" "topology"
  sorry

definition topspace :: "'a topology ⇒ 'a set"
  where ‹topspace = undefined›

definition openin :: ‹'a topology ⇒ 'a set ⇒ bool›
  where ‹openin = undefined›

lemma openin_Int[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∩ T)"
  sorry

lemma ‹¬ (∀veriT_vr79::'a.
                veriT_vr79 ∈ topspace (X::'a topology) ⟶
                veriT_vr79 ∈ topspace X ∧
                (∀veriT_vr80::'a. veriT_vr80 ∈ topspace X ⟶ (f::'a ⇒ 'b) veriT_vr80 ∈ topspace (Y::'b topology)) ∧
                (∀veriT_vr81::'b set.
                    openin Y veriT_vr81 ∧ f veriT_vr79 ∈ veriT_vr81 ⟶
                    (∃veriT_vr82::'a set. openin X veriT_vr82 ∧ veriT_vr79 ∈ veriT_vr82 ∧ (∀veriT_vr83::'a. veriT_vr83 ∈ veriT_vr82 ⟶ f veriT_vr83 ∈ veriT_vr81)))) ∨
         (∀(veriT_vr79::'a) veriT_vr80::'a. veriT_vr79 ∉ topspace X ∨ veriT_vr80 ∉ topspace X ∨ f veriT_vr80 ∈ topspace Y) 
    ›
  by (ctxt_tactic "qnt_cnf")

lemma ‹¬ (∀veriT_vr13 veriT_vr14 veriT_vr15.
                inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) =
                (if 0 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15
                 else if 1 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s1 veriT_vr13 veriT_vr15
                      else if 2 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s2 veriT_vr13 veriT_vr15
                           else if 3 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s3 veriT_vr13 veriT_vr15
                                else if 4 = veriT_vr14 then inv_tm_skip_first_arg_len_eq_1_s4 veriT_vr13 veriT_vr15
                                     else 5 = veriT_vr14 ∧ inv_tm_skip_first_arg_len_eq_1_s5 veriT_vr13 veriT_vr15)) ∨
         (∀veriT_vr13 veriT_vr14 veriT_vr15.
             ¬ inv_tm_skip_first_arg_len_eq_1 veriT_vr13 (veriT_vr14, veriT_vr15) ∨ 0 ≠ veriT_vr14 ∨ inv_tm_skip_first_arg_len_eq_1_s0 veriT_vr13 veriT_vr15)›
  by (ctxt_tactic "qnt_cnf")

end

lemma ‹¬ (∀veriT_vr207 veriT_vr208.
                (stfx_rel veriT_vr207 veriT_vr208 ⟶
                 fst veriT_vr207 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧
                 fst veriT_vr208 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧
                 snd veriT_vr207 ∈ 𝒪⇩Y (fst veriT_vr207) ∧
                 snd veriT_vr208 ∈ 𝒪⇩Y (fst veriT_vr208) ∧
                 (∃veriT_vr209. veriT_vr209 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧ veriT_vr209 ⊆ fst veriT_vr207 ∩ fst veriT_vr208 ∧ ρ⇩Y (fst veriT_vr207) veriT_vr209 (snd veriT_vr207) = ρ⇩Y (fst veriT_vr208) veriT_vr209 (snd veriT_vr208))) ∧
                (fst veriT_vr207 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧
                 fst veriT_vr208 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧
                 snd veriT_vr207 ∈ 𝒪⇩Y (fst veriT_vr207) ∧
                 snd veriT_vr208 ∈ 𝒪⇩Y (fst veriT_vr208) ∧
                 ¬ (∀veriT_vr210. ¬ (veriT_vr210 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu} ∧ veriT_vr210 ⊆ fst veriT_vr207 ∩ fst veriT_vr208 ∧ ρ⇩Y (fst veriT_vr207) veriT_vr210 (snd veriT_vr207) = ρ⇩Y (fst veriT_vr208) veriT_vr210 (snd veriT_vr208))) ⟶
                 stfx_rel veriT_vr207 veriT_vr208)) ∨
         (∀veriT_vr207 veriT_vr208. ¬ stfx_rel veriT_vr207 veriT_vr208 ∨ fst veriT_vr208 ∈ {uu. is_open⇩Y uu ∧ f x ∈ uu}) ›
  by (ctxt_tactic "qnt_cnf")
end

experiment
begin
abbreviation (input)
 "fishburn (a::_::linorder) b v ab ==
  ((ab ≤ a ⟶ v ≤ ab) ∧ (a < ab ∧ ab < b ⟶ ab = v) ∧ (b ≤ ab ⟶ ab ≤ v))"

abbreviation  (input)fishburn2 :: "('a::linorder) ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(_ ≤/ _/ '(mod _,_'))› [51,51,0,0])
  where "fishburn2 ab v a b ≡ fishburn a b v ab"

abbreviation (input)
 "knuth (a::_::linorder) b x y ==
  ((y ≤ a ⟶ x ≤ a) ∧ (a < y ∧ y < b ⟶ y = x) ∧ (b ≤ y ⟶ b ≤ x))"

abbreviation (input) knuth2 :: "('a::linorder) ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(_ ≅/ _/ '(mod _,_'))› [51,51,0,0])
  where "knuth2 x y a b ≡ knuth a b x y"


lemma ‹¬ (∀(veriT_vr28::'a::{linorder}) (veriT_vr29::'a) (veriT_vr30::'a) veriT_vr31::'a. veriT_vr28 ≤ veriT_vr30 (mod veriT_vr29,veriT_vr31) ⟶ veriT_vr30 ≅ veriT_vr28 (mod veriT_vr29,veriT_vr31)) ∨
         (∀(veriT_vr28::'a) (veriT_vr30::'a) veriT_vr31::'a. ¬ veriT_vr30 ≤ veriT_vr28 ∨ veriT_vr28 < veriT_vr31 ∨ ¬ veriT_vr28 ≤ veriT_vr30 ∨ ¬ veriT_vr31 ≤ veriT_vr28 ∨ veriT_vr31 ≤ veriT_vr30) ›
  supply [[simp_trace=false,simp_trace_depth_limit=5]]  by (ctxt_tactic "qnt_cnf")

lemma ‹¬ (∀(veriT_vr2::'a::{one, zero} set) veriT_vr3.
                ((veriT_vr3 ∈ U ⟶ veriT_vr3 ∈ topspace X ∧ 0 ∈ veriT_vr2) ∧ (veriT_vr3 ∉ U ⟶ veriT_vr3 ∈ topspace X ∧ 1 ∈ veriT_vr2)) =
                ((veriT_vr3 ∈ U ⟶ veriT_vr3 ∈ topspace X ∧ 0 ∈ veriT_vr2) ∧ (veriT_vr3 ∉ U ⟶ veriT_vr3 ∈ topspace X ∧ 1 ∈ veriT_vr2))) ∨
         (∀(veriT_vr2::'a::{one, zero} set) veriT_vr3.
             veriT_vr3 ∈ U ∨
             veriT_vr3 ∉ topspace X ∨
             1 ∉ veriT_vr2 ∨ (veriT_vr3 ∈ U ⟶ veriT_vr3 ∈ topspace X ∧ 0 ∈ veriT_vr2) ∧ (veriT_vr3 ∉ U ⟶ veriT_vr3 ∈ topspace X ∧ 1 ∈ veriT_vr2)) ›
  by (ctxt_tactic "qnt_cnf")

lemma ‹ ¬ (∀(veriT_vr24:: 'a set) veriT_vr25. (veriT_vr24 ⊆ veriT_vr25) = (veriT_vr24 = veriT_vr25 ∩ veriT_vr24)) ∨
         (∀(veriT_vr24:: 'a set) veriT_vr25. veriT_vr24 ≠ veriT_vr25 ∩ veriT_vr24 ∨ veriT_vr24 ⊆ veriT_vr25) ›
  by (ctxt_tactic "qnt_cnf")

(* Rule 30: and *)

lemma and_1:
  assumes "a ∧ b ∧ c"
  shows  "a"
  using assms
  by (ctxt_tactic "and" "0::int")

lemma and_2:
  assumes "a ∧ b ∧ c"
  shows  "c"
  using assms
  by (ctxt_tactic "and" "2::int")

lemma and_3:
  assumes "(a ∧ d) ∧ b ∧ c"
  shows  "(a ∧ d)"
  using assms
  by (ctxt_tactic "and" "0::int")

lemma and_4:
  assumes "a ∧ b ∧ (c ∧ d)"
  shows  "c ∧ d"
  using assms
  by (ctxt_tactic "and" "2::int")

lemma and_5:
  assumes "a"
  shows "a"
  using assms
  by (ctxt_tactic "and" "0::int")

(* Rule 31: not_or *)

lemma not_or_1:
  assumes "¬(a ∨ b ∨ c)"
  shows  "¬a"
  using assms
  by (ctxt_tactic "not_or" "0::int")

lemma not_or_2:
  assumes "¬(a)"
  shows  "¬a"
  using assms
  by (ctxt_tactic "not_or" "0::int")

lemma not_or_3:
  assumes "¬((a ∨ d) ∨ b ∨ c)"
  shows  "¬(a ∨ d)"
  using assms
  by (ctxt_tactic "not_or" "0::int")

lemma not_or_4:
  assumes "¬(a ∨ b ∨ (c ∨ d))"
  shows  "¬(c ∨ d)"
  using assms
  by (ctxt_tactic "not_or" "2::int")

lemma not_or_5:
  assumes "¬(a ∨ b ∨ ¬(c ∨ d))"
  shows  "¬(¬(c ∨ d))"
  using assms
  by (ctxt_tactic "not_or" "2::int")

lemma not_or_6:
  assumes " ¬ ((¬ (¬ 1 ≤ a ∧ 1 ≤ b ∧ 1 ≤ c) ∨
             1 ≤ b ∨ 1 ≤ c))"
  shows "¬ ¬ (¬ 1 ≤ a ∧ 1 ≤ b ∧ 1 ≤ c)"
  using assms
  by (ctxt_tactic "not_or" "0::int")

(* Rule 32: or *)

lemma or_1:
  assumes "(a ∨ b ∨ c)"
  shows  "(a ∨ b ∨ c)"
  using assms
  by (ctxt_tactic "or")

lemma or_2:
  assumes "(a)"
  shows  "a"
  using assms
  by (ctxt_tactic "or")

lemma or_3:
  assumes "((a ∨ d) ∨ b ∨ c)"
  shows  "(a ∨ d) ∨ b ∨ c"
  using assms
  by (ctxt_tactic "or" "0::int")


(* Rule 33: weakening *)

lemma weakening_1: 
  assumes "a"
  shows  "a ∨ b"
  using assms
  by (ctxt_tactic "weakening")

lemma weakening_2:
  assumes "a ∨ b ∨ c"
  shows  "a ∨ b ∨ c ∨ d ∨ e"
  using assms
  by (ctxt_tactic "weakening")

lemma weakening_3:
  assumes "a ∨ b ∨ c"
  shows  "a ∨ b ∨ c ∨ c ∨ a"
  using assms
  by (ctxt_tactic "weakening")

lemma weakening_4:
  assumes "(a ∨ b) ∨ b ∨ c"
  shows  "(a ∨ b) ∨ b ∨ c ∨ (c ∨ a) ∨ e"
  using assms
  by (ctxt_tactic "weakening")

lemma weakening_5: 
  assumes "a ∨ ¬f"
  shows  "a ∨ b ∨ ¬f"
  using assms
  by (ctxt_tactic "weakening")


(* Rule 34: reordering *)

lemma reordering_1: 
  assumes "b ∨ a"
  shows "a ∨ b"
  using assms
  by (ctxt_tactic "reordering")

lemma reordering_2:
  assumes "a ∨ b ∨ c"
  shows "c ∨ b ∨ a"
  using assms
  by (ctxt_tactic "reordering")

lemma reordering_3:
  assumes "a ∨ b ∨ a"
  shows "a ∨ a ∨ b"
  using assms
  by (ctxt_tactic "reordering")

lemma reordering_4:
  assumes "(a ∨ b) ∨ a ∨ b"
  shows "a ∨ b ∨ (a ∨ b)"
  using assms
  by (ctxt_tactic "reordering")

(* Rule 34: shuffle *)

lemma shuffle_or_1: 
  shows "(b ∨ a) = (a ∨ b)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_2:
  shows "(a ∨ b) = (a ∨ b)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_3: 
  shows "(a ∨ b ∨ c) = (c ∨ a ∨ b)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_4: 
  shows "(a ∨ b ∨ c) = (a ∨ b ∨ c)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_5: 
  shows "(a ∨ b ∨ c ∨ d) = (c ∨ d ∨ b ∨ a)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_6: 
  shows "(a ∨ (b ∨ c) ∨ d) = ((b ∨ c) ∨ d ∨ a)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_7: 
  shows "(a ∨ b ∨ (c ∨ d)) = (a ∨ (c ∨ d) ∨ b)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_or_8: 
  shows "(a ∨ b ∨ (c ∧ (d ∨ e))) = (a ∨ (c ∧ (d ∨ e)) ∨ b)"
  by (ctxt_tactic "shuffle" "HOL.disj")

lemma shuffle_and_1: 
  shows "(b ∧ a) = (a ∧ b)"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_2: 
  shows "(a ∧ a) = (a ∧ a)"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_3: 
  shows "(a ∧ b ∧ c) = (b ∧ a ∧ c)"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_4: 
  shows "((a ⟶ b ) ∧ c) = (c ∧ (a ⟶ b))"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_5: 
  shows "(d ∧ (a ∨ b ) ∧ c) = (c ∧ d ∧ (a ∨ b))"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_6a:
  shows "(¬ a ∧ ¬ b ∧ c ∧ d) = (c ∧ d ∧ ¬ a ∧ ¬ b)"
  by (ctxt_tactic "shuffle" "HOL.conj")

lemma shuffle_and_6b:
  shows "(¬ (c ∧ a) ∧ ¬ (d ∧ b) ∧ c ∧ a) =
         (c ∧ a ∧ ¬ (c ∧ a) ∧ ¬ (d ∧ b))"
  by (ctxt_tactic "shuffle" "HOL.conj")

(* Rule 36: not_and *)

lemma not_and_1: 
  assumes "¬(a ∧ b ∧ c)"
  shows "¬a ∨ ¬b ∨ ¬c"
  using assms
  by (ctxt_tactic "not_and")

lemma not_and_2:
  assumes "¬a"
  shows "¬a"
  using assms
  by (ctxt_tactic "not_and")

lemma not_and_3:
  assumes "¬((a ∧ d) ∧ b ∧ c)"
  shows "¬(a ∧ d) ∨ ¬b ∨ ¬c"
  using assms
  by (ctxt_tactic "not_and")

lemma not_and_4:
  assumes "¬(a ∧ b ∧ c ∧ (a ∧ d))"
  shows "¬a ∨ ¬b ∨ ¬c ∨ ¬(a ∧ d)"
  using assms
  by (ctxt_tactic "not_and")

lemma not_and_5:
  assumes "¬(a ∧ a ∧ a)"
  shows "¬a ∨ ¬a ∨ ¬a"
  using assms
  by (ctxt_tactic "not_and")


(* Rule 37: xor1 *)

lemma xor1_1: 
  assumes "¬(a = b)"
  shows  "a ∨ b"
  using assms
  by (ctxt_tactic "xor1")

lemma xor1_2:
  assumes "¬((a ∨ b) = b)"
  shows  "(a ∨ b) ∨ b"
  using assms
  by (ctxt_tactic "xor1")

lemma xor1_3:
  assumes "¬((¬(a = b)) = b)"
  shows  "(¬(a = b)) ∨ b"
  using assms
  by (ctxt_tactic "xor1")

lemma xor1_4:
  assumes "¬((a = b) = (¬(b = c)))"
  shows  "(a = b) ∨ (¬(b = c))"
  using assms
  by (ctxt_tactic "xor1")


(* Rule 38: xor2 *)

lemma xor2_1: 
  assumes "¬(a = b)"
  shows  "¬a ∨ ¬b"
  using assms
  by (ctxt_tactic "xor2")

lemma xor2_2:
  assumes "¬((a ∨ b) = b)"
  shows  "¬(a ∨ b) ∨ ¬b"
  using assms
  by (ctxt_tactic "xor2")

lemma xor2_3:
  assumes "¬((a = b) = b)"
  shows  "¬(a = b) ∨ ¬b"
  using assms
  by (ctxt_tactic "xor2")

lemma xor2_4:
  assumes "¬((¬(a = b)) = (¬(b = c)))"
  shows  "¬(¬(a = b)) ∨ ¬(¬(b = c))"
  using assms
  by (ctxt_tactic "xor2")


(* Rule 39: not_xor1 *)

lemma not_xor1_1: 
  assumes "¬(¬(a = b))"
  shows  "a ∨ ¬b"
  using assms
  by (ctxt_tactic "not_xor1")

lemma not_xor1_2:
  assumes "¬(¬((a ∨ b) = b))"
  shows  "(a ∨ b) ∨ ¬b"
  using assms
  by (ctxt_tactic "not_xor1")

lemma not_xor1_3:
  assumes "¬(¬((a = b) = b))"
  shows  "(a = b) ∨ ¬b"
  using assms
  by (ctxt_tactic "not_xor1")

lemma not_xor1_4:
  assumes "¬(¬((¬(a = b)) = (¬(b = c))))"
  shows  "(¬(a = b)) ∨ (¬(¬(b = c)))"
  using assms
  by (ctxt_tactic "not_xor1")


(* Rule 40: not_xor2 *)

lemma not_xor2_1: 
  assumes "¬(¬(a = b))"
  shows  "¬a ∨ b"
  using assms
  by (ctxt_tactic "not_xor2")

lemma not_xor2_2:
  assumes "¬(¬((a ∨ b) = b))"
  shows  "¬(a ∨ b) ∨ b"
  using assms
  by (ctxt_tactic "not_xor2")

lemma not_xor2_3:
  assumes "¬(¬((a = b) = b))"
  shows  "¬(a = b) ∨ b"
  using assms
  by (ctxt_tactic "not_xor2")

lemma not_xor2_4:
  assumes "¬(¬((¬(a = b)) = (¬(b = c))))"
  shows  "(¬(¬(a = b))) ∨ (¬(b = c))"
  using assms
  by (ctxt_tactic "not_xor2")


(* Rule 41: implies *)

lemma implies_1: 
  assumes "(a ⟶ b)"
  shows  "¬a ∨ b"
  using assms
  by (ctxt_tactic "implies")

lemma implies_2:
  assumes "((a∨b) ⟶ b)"
  shows  "¬(a∨b) ∨ b"
  using assms
  by (ctxt_tactic "implies")

lemma implies_3:
  assumes "((a⟶b) ⟶ b)"
  shows  "¬(a⟶b) ∨ b"
  using assms
  by (ctxt_tactic "implies")

lemma implies_4:
  assumes "((a⟶b) ⟶ (b ⟶ c))"
  shows  "¬(a⟶b) ∨ (b ⟶ c)"
  using assms
  by (ctxt_tactic "implies")

lemma implies_5:
  assumes "((¬(a⟶b)) ⟶ (b ⟶ c))"
  shows  "¬(¬(a⟶b)) ∨ (b ⟶ c)"
  using assms
  by (ctxt_tactic "implies")


(* Rule 42: not_implies1 *)

lemma not_implies1_1: 
  assumes "¬(a ⟶ b)"
  shows  "a"
  using assms
  by (ctxt_tactic "not_implies1")

lemma not_implies1_2:
  assumes "¬((a∨b) ⟶ b)"
  shows  "(a∨b)"
  using assms
  by (ctxt_tactic "not_implies1")

lemma not_implies1_3:
  assumes "¬((a⟶b) ⟶ b)"
  shows  "(a⟶b)"
  using assms
  by (ctxt_tactic "not_implies1")

lemma not_implies1_4:
  assumes "¬((a⟶b) ⟶ (b ⟶ c))"
  shows  "(a⟶b)"
  using assms
  by (ctxt_tactic "not_implies1")

lemma not_implies1_5:
  assumes "¬((¬(a⟶b)) ⟶ (b ⟶ c))"
  shows  "(¬(a⟶b))"
  using assms
  by (ctxt_tactic "not_implies1")


(* Rule 43: not_implies2 *)

lemma not_implies2_1: 
  assumes "¬(a ⟶ b)"
  shows  "¬b"
  using assms
  by (ctxt_tactic "not_implies2")

lemma not_implies2_2:
  assumes "¬((a∨b) ⟶ b)"
  shows  "¬b"
  using assms
  by (ctxt_tactic "not_implies2")

lemma not_implies2_3:
  assumes "¬(a ⟶ (a⟶b))"
  shows  "¬(a⟶b)"
  using assms
  by (ctxt_tactic "not_implies2")

lemma not_implies2_4:
  assumes "¬((a ⟶ b) ⟶ (b ⟶ c))"
  shows  "¬(b ⟶ c)"
  using assms
  by (ctxt_tactic "not_implies2")

lemma not_implies2_5:
  assumes "¬((a ⟶ b) ⟶ (¬(b ⟶ c)))"
  shows  "¬(¬(b ⟶ c))"
  using assms
  by (ctxt_tactic "not_implies2")


(* Rule 44: equiv1 *)

lemma equiv1_1: 
  assumes "(a = b)"
  shows  "¬a ∨ b"
  using assms
  by (ctxt_tactic "equiv1")

lemma equiv1_2:
  assumes "((a∨b) = b)"
  shows  "¬(a∨b) ∨ b"
  using assms
  by (ctxt_tactic "equiv1")

lemma equiv1_3:
  assumes "((a=b) = b)"
  shows  "¬(a=b) ∨ b"
  using assms
  by (ctxt_tactic "equiv1")

lemma equiv1_4:
  assumes "((a=b) = (b = c))"
  shows  "¬(a=b) ∨ (b = c)"
  using assms
  by (ctxt_tactic "equiv1")

lemma equiv1_5:
  assumes "((¬(a=b)) = (b = c))"
  shows  "¬(¬(a=b)) ∨ (b = c)"
  using assms
  by (ctxt_tactic "equiv1")


(* Rule 44: equiv2 *)

lemma equiv2_1: 
  assumes "(a = b)"
  shows  "a ∨ ¬b"
  using assms
  by (ctxt_tactic "equiv2")

lemma equiv2_2:
  assumes "((a∨b) = b)"
  shows  "(a∨b) ∨ ¬b"
  using assms
  by (ctxt_tactic "equiv2")

lemma equiv2_3:
  assumes "((a=b) = b)"
  shows  "(a=b) ∨ ¬b"
  using assms
  by (ctxt_tactic "equiv2")

lemma equiv2_4:
  assumes "((a=b) = (b = c))"
  shows  "(a=b) ∨ ¬(b = c)"
  using assms
  by (ctxt_tactic "equiv2")

lemma equiv2_5:
  assumes "((a=b) = (¬(b = c)))"
  shows  "(a=b) ∨ ¬(¬(b = c))"
  using assms
  by (ctxt_tactic "equiv2")


(* Rule 46: not_equiv1 *)

lemma not_equiv1_1: 
  assumes "¬(a = b)"
  shows  "a ∨ b"
  using assms
  by (ctxt_tactic "not_equiv1")

lemma not_equiv1_2:
  assumes "¬((a∨b) = b)"
  shows  "(a∨b) ∨ b"
  using assms
  by (ctxt_tactic "not_equiv1")

lemma not_equiv1_3:
  assumes "¬((a=b) = b)"
  shows  "(a=b) ∨ b"
  using assms
  by (ctxt_tactic "not_equiv1")

lemma not_equiv1_4:
  assumes "¬((a=b) = (b = c))"
  shows  "(a=b) ∨ (b = c)"
  using assms
  by (ctxt_tactic "not_equiv1")

lemma not_equiv1_5:
  assumes "¬((a=b) = (¬(b = c)))"
  shows  "(a=b) ∨ ¬(b = c)"
  using assms
  by (ctxt_tactic "not_equiv1")


(* Rule 47: not_equiv2 *)

lemma not_equiv2_1: 
  assumes "¬(a = b)"
  shows  "¬a ∨ ¬b"
  using assms
  by (ctxt_tactic "not_equiv2")

lemma not_equiv2_2:
  assumes "¬((a∨b) = b)"
  shows  "¬(a∨b) ∨ ¬b"
  using assms
  by (ctxt_tactic "not_equiv2")

lemma not_equiv2_3:
  assumes "¬((a=b) = b)"
  shows  "¬(a=b) ∨ ¬b"
  using assms
  by (ctxt_tactic "not_equiv2")

lemma not_equiv2_4:
  assumes "¬((a=b) = (b = c))"
  shows  "¬(a=b) ∨ ¬(b = c)"
  using assms
  by (ctxt_tactic "not_equiv2")

lemma not_equiv2_5:
  assumes "¬((a=b) = (¬(b = c)))"
  shows  "¬(a=b) ∨ ¬(¬(b = c))"
  using assms
  by (ctxt_tactic "not_equiv2")


(* Rule 48: and_pos *)

lemma "¬(a ∧ b ∧ c) ∨ c"
  by (ctxt_tactic "and_pos" "2")

lemma and_pos_1: "¬(a ∧ b ∧ c) ∨ b"
  by (ctxt_tactic "and_pos" "1")

lemma and_pos_2: "¬(a ∧ b ∧ c) ∨ c"
  by (ctxt_tactic "and_pos" "2")

lemma and_pos_3: "¬(a ∧ (b ∧ c) ∧ d) ∨ (b ∧ c)"
  by (ctxt_tactic "and_pos" "1")

lemma and_pos_4: "¬(a ∧ (b ∧ c) ∧ d) ∨ d"
  by (ctxt_tactic "and_pos" "2")

lemma and_pos_5: "¬(a ∧ (b ∨ ¬c ∧ d)) ∨ (b ∨ ¬c ∧ d)"
  by (ctxt_tactic "and_pos" "1")

lemma and_pos_6: "¬(a ∧ (b ∧ c)) ∨ (b ∧ c)"
  by (ctxt_tactic "and_pos" "1")

lemma and_pos_7: "¬((¬a ∨ b) ∧ c) ∨ (¬a ∨ b)"
  by (ctxt_tactic "and_pos" "0")

lemma and_pos_8: "¬(a ∧ ¬b) ∨ ¬b"
  by (ctxt_tactic "and_pos" "1")

lemma and_pos_9: "¬(a) ∨ a"
  by (ctxt_tactic "and_pos" "0")

(* Rule 48: and_neg *)

lemma and_neg_1: "(a ∧ b) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "and_neg")

lemma and_neg_2: "(a ∧ b ∧ c) ∨ ¬a ∨ ¬b ∨ ¬c"
  by (ctxt_tactic "and_neg")

lemma and_neg_3: "(a ∧ b ∧ c ∧ d) ∨ ¬a ∨ ¬b ∨ ¬c ∨ ¬d"
  by (ctxt_tactic "and_neg")

lemma and_neg_4: "(a ∧ (b ∧ c)) ∨ ¬a ∨ ¬(b ∧ c)"
  by (ctxt_tactic "and_neg")

lemma and_neg_5: "((a ∧ b) ∧ d) ∨ ¬(a ∧ b) ∨ ¬d"
  by (ctxt_tactic "and_neg")

lemma and_neg_6: "(a ∧ d) ∨ ¬(a ∧ d)"
  by (ctxt_tactic "and_neg")

lemma and_neg_7: "((a = c) ∧ (b ⟶ ¬c ∨ d)) ∨ ¬(a = c) ∨ ¬(b ⟶ ¬c ∨ d)"
  by (ctxt_tactic "and_neg")

lemma and_neg_8: "(¬a ∧ ¬(b ∨ c) ∧ d) ∨ ¬¬a ∨ ¬¬(b ∨ c) ∨ ¬d"
  by (ctxt_tactic "and_neg")

lemma and_neg_9: "a ∨ (¬a)"
  by (ctxt_tactic "and_neg")

(* Rule 50: or_pos *)

lemma or_pos_1: "¬(a ∨ b) ∨ a ∨ b"
  by (ctxt_tactic "or_pos")

lemma or_pos_2: "¬(a ∨ b ∨ c) ∨ a ∨ b ∨ c"
  by (ctxt_tactic "or_pos")

lemma or_pos_3: "¬(a ∨ b ∨ c ∨ d) ∨ a ∨ b ∨ c ∨ d"
  by (ctxt_tactic "or_pos")

lemma or_pos_4: "¬(a ∨ (b ∨ c)) ∨ a ∨ b ∨ c"
  by (ctxt_tactic "or_pos")

lemma or_pos_5: "¬((a ∨ b) ∨ c) ∨ (a ∨ b) ∨ c"
  by (ctxt_tactic "or_pos")

lemma or_pos_6: "¬(¬(e ∨ f) ∨ (a ∨ b ∧ c) ∨ d) ∨ ¬(e ∨ f) ∨ (a ∨ b ∧ c) ∨ d"
  by (ctxt_tactic "or_pos")

lemma or_pos_7: "¬(a) ∨ a"
  by (ctxt_tactic "or_pos")

(* Rule 51: or_neg *)

lemma or_neg_1: "(a ∨ b ∨ c) ∨ ¬a"
  by (ctxt_tactic "or_neg" "0::int")

lemma or_neg_2: "(a ∨ b ∨ c) ∨ ¬b"
  by (ctxt_tactic "or_neg" "1")

lemma or_neg_3: "(a ∨ b ∨ c) ∨ ¬c"
  by (ctxt_tactic "or_neg" "2")

lemma or_neg_4: "((a ∨ b) ∨ c) ∨ ¬(a ∨ b)"
  by (ctxt_tactic "or_neg" "0")

lemma or_neg_5: "(a ∨ (b ∨ c) ∨ d) ∨ ¬(b ∨ c)"
  by (ctxt_tactic "or_neg" "1")

lemma or_neg_6: "(a ∨ b ∨ (c ∨ d)) ∨ ¬(c ∨ d)"
  by (ctxt_tactic "or_neg" "2")

lemma or_neg_7: "((a ∧ b) ∨ b ∨ (¬c ⟶ d)) ∨ ¬(¬c ⟶ d)"
  by (ctxt_tactic "or_neg" "2")

lemma or_neg_8: "((a ∧ b) ∨ b ∨ ¬(c ⟶ d)) ∨ ¬(¬(c ⟶ d))"
  by (ctxt_tactic "or_neg" "2")

lemma or_neg_9: "(¬a ∨ b ∨ c) ∨ ¬(¬a)"
  by (ctxt_tactic "or_neg" "0")

lemma or_neg_10: "(¬a ∨ b) ∨ ¬(¬a)"
  by (ctxt_tactic "or_neg" "0")

lemma or_neg_11: "(¬a ∨ b) ∨ ¬b"
  by (ctxt_tactic "or_neg" "1")

lemma or_neg_12: "(a) ∨ ¬a"
  by (ctxt_tactic "or_neg" "0")

(* Rule 52: xor_pos1 *)

lemma xor_pos1_1: "¬(a ≠ b) ∨ a ∨ b"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_2: "¬((a∨c) ≠ b) ∨ (a∨c) ∨ b"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_3: "¬((a∧c) ≠ b) ∨ (a∧c) ∨ b"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_4: "¬(a ≠ (b ∧ c)) ∨ a ∨ (b ∧ c)"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_5: "¬((a ∧ b) ≠ ((c ∨ d))) ∨ (a ∧ b) ∨ (c ∨ d)"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_6: "¬((¬a) ≠ b) ∨ ¬a ∨ b"
  by (ctxt_tactic "xor_pos1")

lemma xor_pos1_7: "¬(a ≠ (¬b)) ∨ a ∨ ¬b"
  by (ctxt_tactic "xor_pos1")

(* Rule 53: xor_pos2 *)

lemma xor_pos2_1: "¬(a ≠ b) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_2: "¬((a∨c) ≠ b) ∨ ¬(a∨c) ∨ ¬b"
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_3: "¬((a∧c) ≠ b) ∨ ¬(a∧c) ∨ ¬b"
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_4: "¬(a ≠ (b ∨ c)) ∨ ¬a ∨ ¬(b ∨ c)"
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_5: "¬((a ∧ b) ≠ (c ∨ d)) ∨ ¬(a ∧ b) ∨ ¬(c ∨ d)"
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_6: ‹¬((¬a) ≠ b) ∨ ¬¬a ∨ ¬b›
  by (ctxt_tactic "xor_pos2")

lemma xor_pos2_7: ‹¬(a ≠ (¬b)) ∨ ¬a ∨ ¬¬b›
  by (ctxt_tactic "xor_pos2")

(* Rule 54: xor_neg1 *)

lemma xor_neg1_1: "(a ≠ b) ∨ a ∨ ¬b"
  by (ctxt_tactic "xor_neg1")

lemma xor_neg1_2: "((a∨c) ≠ b) ∨ (a∨c) ∨ ¬b"
  by (ctxt_tactic "xor_neg1")

lemma xor_neg1_3: "(b ≠ (a∧c)) ∨ b ∨ ¬(a∧c)"
  by (ctxt_tactic "xor_neg1")

lemma xor_neg1_4: "(a ≠ (¬b)) ∨ a ∨ ¬¬b"
  by (ctxt_tactic "xor_neg1")

lemma xor_neg1_5: "((¬a) ≠ b) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "xor_neg1")

(* Rule 55: xor_neg2 *)

lemma xor_neg2_1: "(a ≠ b) ∨ ¬a ∨ b"
  by (ctxt_tactic "xor_neg2")

lemma xor_neg2_2: "((a∨c) ≠ b) ∨ ¬(a∨c) ∨ b"
  by (ctxt_tactic "xor_neg2")

lemma xor_neg2_3: "(b ≠ (a∧c)) ∨ ¬b ∨ (a∧c)"
  by (ctxt_tactic "xor_neg2")

lemma xor_neg2_4: "(a ≠ (¬b)) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "xor_neg2")

lemma xor_neg2_5: "((¬a) ≠ b) ∨ ¬¬a ∨ b"
  by (ctxt_tactic "xor_neg2")

(* Rule 56: implies_pos *)

lemma implies_pos_1: "¬(a ⟶ b) ∨ ¬a ∨ b"
  by (ctxt_tactic "implies_pos")

lemma implies_pos_2: "¬(p ⟶ ¬q) ∨ ¬p ∨ ¬q"
  by (ctxt_tactic "implies_pos")

lemma implies_pos_3: ‹¬(¬p ⟶ q) ∨ ¬¬p ∨ q›
  by (ctxt_tactic "implies_pos")

lemma implies_pos_4:  "¬((a ∧ b) ⟶ c) ∨ ¬(a ∧ b) ∨ c"
  by (ctxt_tactic "implies_pos")

lemma implies_pos_5: "¬((a ⟶ b) ⟶ c) ∨ ¬(a ⟶ b) ∨ c"
  by (ctxt_tactic "implies_pos")

lemma implies_pos_6: "¬((a ⟶ b) ⟶ (c ⟶ d)) ∨ ¬(a ⟶ b) ∨ (c ⟶ d)"
  by (ctxt_tactic "implies_pos")

(* Rule 57: implies_neg1 *)

lemma implies_neg1_1: "(a ⟶ b) ∨ a"
  by (ctxt_tactic "implies_neg1")

lemma implies_neg1_2:  "((a ∧ b) ⟶ c) ∨ (a ∧ b)"
  by (ctxt_tactic "implies_neg1")

lemma implies_neg1_3: "((a ⟶ b) ⟶ c) ∨ (a ⟶ b)"
  by (ctxt_tactic "implies_neg1")

lemma implies_neg1_4: "((a ⟶ b) ⟶ (c ⟶ d)) ∨ (a ⟶ b)"
  by (ctxt_tactic "implies_neg1")

lemma implies_neg1_5: "((a = b) ⟶ b) ∨ (a = b)"
  by (ctxt_tactic "implies_neg1")

lemma implies_neg1_6: "(¬(a = b) ⟶ b) ∨ ¬(a = b)"
  by (ctxt_tactic "implies_neg1")

(* Rule 58: implies_neg2 *)

lemma implies_neg2_1: "(a ⟶ b) ∨ ¬b"
  by (ctxt_tactic "implies_neg2")

lemma implies_neg2_2:  "((a ∧ b) ⟶ c) ∨ ¬c"
  by (ctxt_tactic "implies_neg2")

lemma implies_neg2_3: "((a ⟶ b) ⟶ c) ∨ ¬c"
  by (ctxt_tactic "implies_neg2")

lemma implies_neg2_4: "((a ⟶ b) ⟶ (c ⟶ d)) ∨ ¬(c ⟶ d)"
  by (ctxt_tactic "implies_neg2")

lemma implies_neg2_5: "(a ⟶ ¬b) ∨ ¬¬b"
  by (ctxt_tactic "implies_neg2")

(* Rule 59: equiv_pos1 *)

lemma equiv_pos1_1: "¬(a = b) ∨ a ∨ ¬b"
  by (ctxt_tactic "equiv_pos1")

lemma equiv_pos1_2: "¬(a = (b = c)) ∨ a ∨ ¬(b = c)"
  by (ctxt_tactic "equiv_pos1")

lemma equiv_pos1_3: "¬((a = d) = (b = c)) ∨ (a = d) ∨ ¬(b = c)"
  by (ctxt_tactic "equiv_pos1")

lemma equiv_pos1_4: "¬((¬a) = b) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "equiv_pos1")

lemma equiv_pos1_5: "¬(a = (¬b)) ∨ a ∨ ¬¬b"
  by (ctxt_tactic "equiv_pos1")

(* Rule 60: equiv_pos2 *)

lemma equiv_pos2_1: "¬(a = b) ∨ ¬a ∨ b"
  by (ctxt_tactic "equiv_pos2")

lemma equiv_pos2_2: "¬(a = (b = c)) ∨ ¬a ∨ (b = c)"
  by (ctxt_tactic "equiv_pos2")

lemma equiv_pos2_3: "¬((a = d) = (b = c)) ∨ ¬(a = d) ∨ (b = c)"
  by (ctxt_tactic "equiv_pos2")

lemma equiv_pos2_4: "¬((¬a) = b) ∨ ¬¬a ∨ b"
  by (ctxt_tactic "equiv_pos2")

lemma equiv_pos2_5: "¬(a = (¬b)) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "equiv_pos2")
end

experiment
  fixes P :: ‹nat ⇒ nat ⇒ bool› and Q :: ‹nat ⇒ bool›
begin
ML ‹
fun generate_term n =
  if n = 0 then @{term ‹0::nat›}
  else @{term ‹Suc›} $ generate_term (n-1)

fun disj m n =
  if m = 0 then @{term Q} $  generate_term n
  else @{term ‹HOL.disj›} $ disj (m-1) n $ disj (m-1) n

val n = 100
val m = 10
val t1 = disj m n
val t2 = @{term Q} $ generate_term n

val ct = 
  @{term ‹Trueprop›} $ (
  @{term ‹HOL.disj›} $
    (@{term ‹Not›} $ (@{term ‹HOL.eq :: bool ⇒ bool ⇒ bool›} $ t1 $ t2)) $
      
    (@{term ‹HOL.disj›} $ (@{term ‹Not›} $ t1) $ t2))
  |> Envir.beta_norm

›

ML ‹
(Alethe_Replay_Methods.equiv_pos2 @{context} [] ct) 
|> Thm.one_prem
›

end
(* Rule 61: equiv_neg1 *)

lemma equiv_neg1_1: "(a = b) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "equiv_neg1")

lemma equiv_neg1_2: "(a = (b = c)) ∨ ¬a ∨ ¬(b = c)"
  by (ctxt_tactic "equiv_neg1")

lemma equiv_neg1_3: "((a = d) = (b = c)) ∨ ¬(a = d) ∨ ¬(b = c)"
  by (ctxt_tactic "equiv_neg1")

lemma equiv_neg1_4: "((¬a) = b) ∨ ¬(¬a) ∨ ¬b"
  by (ctxt_tactic "equiv_neg1")

lemma equiv_neg1_5: "(a = (¬b)) ∨ ¬a ∨ ¬(¬b)"
  by (ctxt_tactic "equiv_neg1")

(* Rule 62: equiv_neg2 *)

lemma equiv_neg2_1: "(a = b) ∨ a ∨ b"
  by (ctxt_tactic "equiv_neg2")

lemma equiv_neg2_2: "(a = (b = c)) ∨ a ∨ (b = c)"
  by (ctxt_tactic "equiv_neg2")

lemma equiv_neg2_3: "((a = d) = (b = c)) ∨ (a = d) ∨ (b = c)"
  by (ctxt_tactic "equiv_neg2")

lemma equiv_neg2_4: "((¬a) = b) ∨ ¬a ∨ b"
  by (ctxt_tactic "equiv_neg2")

lemma equiv_neg2_5: "(a = (¬b)) ∨ a ∨ ¬b"
  by (ctxt_tactic "equiv_neg2")

(* Rule 63: ite1 *)

lemma ite1_1: 
  assumes "(If a b c)"
  shows "a ∨ c"
  using assms
  by (ctxt_tactic "ite1")

lemma ite1_2: 
  assumes "(If (If e d f) b c)"
  shows "(If e d f) ∨ c"
  using assms
  by (ctxt_tactic "ite1")

lemma ite1_3: 
  assumes "(If a b (If e d f))"
  shows "a ∨ (If e d f)"
  using assms
  by (ctxt_tactic "ite1")

(* Rule 64: ite2 *)

lemma ite2_1: 
  assumes "(If a b c)"
  shows "¬a ∨ b"
  using assms
  by (ctxt_tactic "ite2")

lemma ite2_2: 
  assumes "(If (If e d f) b c)"
  shows "¬(If e d f) ∨ b"
  using assms
  by (ctxt_tactic "ite2")

lemma ite2_3: 
  assumes "(If a b (If e d f))"
  shows "¬a ∨ b"
  using assms
  by (ctxt_tactic "ite2")

(* Rule 65: ite_pos1 *)

lemma ite_pos1_1: "¬(If a b c) ∨ a ∨ c"
  by (ctxt_tactic "ite_pos1")

lemma ite_pos1_2: "¬(If a b (a ∨ c)) ∨ a ∨ (a ∨ c)"
  by (ctxt_tactic "ite_pos1")

lemma ite_pos1_3: "¬(If a b (d ∨ c)) ∨ a ∨ (d ∨ c)"
  by (ctxt_tactic "ite_pos1")

lemma ite_pos1_4: "¬(If a b (If a b c)) ∨ a ∨ (If a b c)"
  by (ctxt_tactic "ite_pos1")

lemma ite_pos1_5: "¬(If (¬a) True (¬(b ∨ c))) ∨ ¬a ∨ ¬(b ∨ c)"
  by (ctxt_tactic "ite_pos1")

lemma ite_pos1_6: "¬(If (¬a) False (b ∧ c)) ∨ ¬a ∨ (b ∧ c)"
  by (ctxt_tactic "ite_pos1")

(* Rule 66: ite_pos2 *)

lemma ite_pos2_1: "¬(If a b c) ∨ ¬a ∨ b"
  by (ctxt_tactic "ite_pos2")

lemma ite_pos2_2: "¬(If a (a ∨ c) b) ∨ ¬a ∨ (a ∨ c)"
  by (ctxt_tactic "ite_pos2")

lemma ite_pos2_3: "¬(If a b (d ∨ c)) ∨ ¬a ∨ b"
  by (ctxt_tactic "ite_pos2")

lemma ite_pos2_4: "¬(If a (If a b c) (If d b c)) ∨ ¬a ∨ (If a b c)"
  by (ctxt_tactic "ite_pos2")

lemma ite_pos2_5: "¬(If (¬a) (¬(b ∨ c)) True) ∨ ¬(¬a) ∨ ¬(b ∨ c)"
  by (ctxt_tactic "ite_pos2")

lemma ite_pos2_6: "¬(If (¬a) (b ∧ c) False) ∨ ¬(¬a) ∨ (b ∧ c)"
  by (ctxt_tactic "ite_pos2")

(* Rule 67: ite_neg1 *)

lemma ite_neg1_1: "(If a b c) ∨ a ∨ ¬c"
  by (ctxt_tactic "ite_neg1")

lemma ite_neg1_2: "(If a b (a ∨ c)) ∨ a ∨ ¬(a ∨ c)"
  by (ctxt_tactic "ite_neg1")

lemma ite_neg1_3: "(If a b (d ∨ c)) ∨ a ∨ ¬(d ∨ c)"
  by (ctxt_tactic "ite_neg1")

lemma ite_neg1_4: "(If a (If a b c) (If d b c)) ∨ a ∨ ¬(If d b c)"
  by (ctxt_tactic "ite_neg1")

lemma ite_neg1_5: "(If (¬a) False (b ∧ c)) ∨ ¬a ∨ ¬(b ∧ c)"
  by (ctxt_tactic "ite_neg1")

(* Rule 68: ite_neg2 *)

lemma ite_neg2_1: "(If a b c) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "ite_neg2")

lemma ite_neg2_2: "(If a b (a ∨ c)) ∨ ¬a ∨ ¬b"
  by (ctxt_tactic "ite_neg2")

lemma ite_neg2_3: "(If a (d ∨ c)  b) ∨ ¬a ∨ ¬(d ∨ c)"
  by (ctxt_tactic "ite_neg2")

lemma ite_neg2_4: "(If a (If a b c) (If d b c)) ∨ ¬a ∨ ¬(If a b c)"
  by (ctxt_tactic "ite_neg2")

lemma ite_neg2_5: "(If (¬a) (b ∧ c) False) ∨ ¬(¬a) ∨ ¬(b ∧ c)"
  by (ctxt_tactic "ite_neg2")

(* Rule 69: not_ite1 *)

lemma not_ite1_1: 
  assumes "¬(If a b c)"
  shows "a ∨ ¬c"
  using assms
  by (ctxt_tactic "not_ite1")

lemma not_ite1_2: 
  assumes "¬(If (If e d f) b c)"
  shows "(If e d f) ∨ ¬c"
  using assms
  by (ctxt_tactic "not_ite1")

lemma not_ite1_3: 
  assumes "¬(If a b (If e d f))"
  shows "a ∨ ¬(If e d f)"
  using assms
  by (ctxt_tactic "not_ite1")

(* Rule 70: not_ite2 *)

lemma not_ite2_1: 
  assumes "¬(If a b c)"
  shows "¬a ∨ ¬b"
  using assms
  by (ctxt_tactic "not_ite2")

lemma not_ite2_2: 
  assumes "¬(If (If e d f) b c)"
  shows "¬(If e d f) ∨ ¬b"
  using assms
  by (ctxt_tactic "not_ite2")

lemma not_ite2_3: 
  assumes "¬(If a b (If e d f))"
  shows "¬a ∨ ¬b"
  using assms
  by (ctxt_tactic "not_ite2")

(* Rule 71: connective_def *)

lemma connective_def_1: "(a ≠ b) = ((¬a ∧ b) ∨ (a ∧ ¬b))"
  by (ctxt_tactic "connective_def")

lemma connective_def_2: "((a = c) ≠ b) = (((¬(a = c)) ∧ b) ∨ ((a = c) ∧ ¬b))"
  by (ctxt_tactic "connective_def")

lemma connective_def_3: "(a = b) = ((a ⟶ b) ∧ (b ⟶ a))"
  by (ctxt_tactic "connective_def")

lemma connective_def_4: "(If a b c) = ((a ⟶ b) ∧ (¬a ⟶ c))"
  by (ctxt_tactic "connective_def")

lemma connective_def_5: "(∀x::'a. y) = (¬(∃x::'a. ¬y))"
  by (ctxt_tactic "connective_def")

lemma connective_def_6: "(∃x::'a. p) = (¬(∀x::'a. ¬p))"
  by (ctxt_tactic "connective_def")

lemma connective_def_7: "(∃(x::'a) y. (x = y)) = (¬(∀(x::'a) y. ¬(x = y)))"
  by (ctxt_tactic "connective_def")

lemma connective_def_8: "(∀(x::'a) y. (x = y)) = (¬(∃(x::'a) y. ¬(x = y)))"
  by (ctxt_tactic "connective_def")

lemma connective_def_9: "(∀x. x ∧ a) = (¬(∃x. ¬(x ∧ a)))"
  by (ctxt_tactic "connective_def")

lemma connective_def_10: "(∀x y. x ∧ y) = (¬(∃x y. ¬(x ∧ y)))"
  by (ctxt_tactic "connective_def")

(* Rule 72: and_simplify *)

lemma and_simplify_1: "(True ∧ True) = True"
  by (ctxt_tactic "and_simplify")

lemma and_simplify_2: "(True ∧ a) = a"
  by (ctxt_tactic "and_simplify")

lemma and_simplify_3: "(True ∧ a ∧ False) = False"
  by (ctxt_tactic "and_simplify")

lemma and_simplify_4: "(True ∧ ¬¬a ∧ b ∧ ¬¬¬a) = False"
  by (ctxt_tactic "and_simplify")

(* Rule 73: or_simplify *)

lemma or_simplify_1: "(True ∨ True) = True"
  by (ctxt_tactic "or_simplify")

lemma or_simplify_2: "(True ∨ a) = True"
  by (ctxt_tactic "or_simplify")

lemma or_simplify_3: "(True ∨ a ∨ False) = True"
  by (ctxt_tactic "or_simplify")

lemma or_simplify_4: "(False ∨ ¬¬a ∨ b ∨ ¬¬¬a) = True"
  by (ctxt_tactic "or_simplify")

(* Rule 74: not_simplify *)

lemma not_simplify_1: "(¬False) = True"
  by (ctxt_tactic "not_simplify")

lemma not_simplify_2: "(¬True) = False"
  by (ctxt_tactic "not_simplify")

lemma not_simplify_3: "(¬¬a) = a"
  by (ctxt_tactic "not_simplify")

lemma not_simplify_4: "(¬¬¬a) = (¬a)"
  by (ctxt_tactic "not_simplify")

lemma not_simplify_5: "(¬¬¬True) = False"
  by (ctxt_tactic "not_simplify")

lemma not_simplify_6: "(¬¬¬False) = True"
  by (ctxt_tactic "not_simplify")

(* Rule 75: implies_simplify *)

lemma implies_simplify_1: "((¬a) ⟶ ¬b) = (b ⟶ a)"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_2: "False ⟶ a = True"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_3: "(a ⟶ True) = True"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_4: "True ⟶ (a = a)"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_5: "(a ⟶ False) = (¬a)"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_6: "(a ⟶ a) = True"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_7: "(¬a ⟶ a) = a"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_8: "(a ⟶ ¬a) = (¬a)"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_9: "((False ⟶ a) ⟶ (¬a)) = (¬a)"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_10: "(False ⟶ False) = True" 
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_11: "(False ⟶ True) = True"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_12: "(True ⟶ False) = False"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_13: "(True ⟶ True) = True"
  by (ctxt_tactic "implies_simplify")

lemma implies_simplify_14: "(False ⟶ ¬False) = True" 
  by (ctxt_tactic "implies_simplify")

(* Rule 76: equiv_simplify *)

lemma equiv_simplify_1: "(¬b = (¬b)) = True"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_2: "(b = (¬b)) = False"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_3: "(¬b = b) = False"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_4: "(True = b) = b"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_5: "(b = True) = b"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_6: "(False = b) = (¬b)"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_7: "(False = b) = (¬b)"
  by (ctxt_tactic "equiv_simplify")

lemma equiv_simplify_8: "((¬a) = (¬b)) = (a = b)"
  by (ctxt_tactic "equiv_simplify")

(* Rule 77: bool_simplify *)

lemma bool_simplify_1:
  shows "(¬(a ⟶ b)) = (a ∧ ¬b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_2: 
  shows "¬(a ∨ b) = (¬a ∧ ¬b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_3: 
  shows "¬(a ∧ b) = (¬a ∨ ¬b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_4:
  shows "(a ⟶ (b ⟶ c)) = ((a ∧ b) ⟶ c)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_5: 
  shows "((a ⟶ b) ⟶ b) = (a ∨ b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_6:
  shows "(a ∧ (a ⟶ b)) = (a ∧ b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_7:
  shows "((a ⟶ b) ∧ a) = (a ∧ b)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_8: (*associativity of ∧ on the LHS.*)
  shows "(a ⟶ b ⟶ c ⟶ d) = (a ∧ b ∧ c ⟶ d)"
  by (ctxt_tactic "bool_simplify")

lemma bool_simplify_9:
  shows ‹(a ⟶ b ⟶ c ⟶ d) = ((a ∧ b) ⟶ c ⟶ d)›
  by (ctxt_tactic "bool_simplify")

(* Rule 78: ac_simp *)

lemma ac_simp_1: "(b ∧ b) = b"
  by (ctxt_tactic "ac_simp")

lemma ac_simp_2: "(b ∧ a ∧ b) = (a ∧ b)"
  by (ctxt_tactic "ac_simp")

lemma ac_simp_3: "(b ∧ a ∧ b) = (a ∧ b)"
  by (ctxt_tactic "ac_simp")

lemma ac_simp_4: "(b ∧ ((a ∧ c) ∧ (d ∧ a))) = (a ∧ b ∧ c ∧ d)"
  by (ctxt_tactic "ac_simp")

(* Rule 79: ite_simplify *)
           
lemma ite_simplify_1:
  shows "(If True a b) = a"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_2:
  shows "(If False a b) = b"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_3:
  shows "(If c b b) = b"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_4:
  shows "(If (¬c) a b) = (If c b a)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_5:
  shows "(If c (If c a b) d) = (If c a d)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_6:
  shows "(If c a (If c b d)) = (If c a d)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_7:
  shows "(If c True False) = c"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_8:
  shows "(If c False True) = (¬c)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_9:
  shows "(If c True d) = (c ∨ d)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_10:
  shows "(If c a False) = (c ∧ a)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_11:
  shows "(If c False a) = (¬c ∧ a)"
  by (ctxt_tactic "ite_simplify")

lemma ite_simplify_12:
  shows "(If c a True) = (¬c ∨ a)"
  by (ctxt_tactic "ite_simplify")

(* Rule 80: qnt_simplify *)

lemma qnt_simplify_1:
  shows "(∀x1. True) = True"
  by (ctxt_tactic "qnt_simplify")

lemma qnt_simplify_2:
  shows "(∀x1 x2. True) = True"
  by (ctxt_tactic "qnt_simplify")

lemma qnt_simplify_3:
  shows "(∀x1. False) = False"
  by (ctxt_tactic "qnt_simplify")

lemma qnt_simplify_4:
  shows "(∀x1 x2. False) = False"
  by (ctxt_tactic "qnt_simplify")

(* Rule 82: qnt_join *)

lemma qnt_join_1:
  shows "(∀x1. a) = (∀x1. a)"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_2:
  shows "(∀x1 . (∀x2. a ∧ x1)) = (∀x1 x2. a ∧ x1)"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_3:
  shows "(∀x1 (x2::'a). (∀x3 x4. (a ∧ x3 ∨ x4 ∧ x1))) = (∀x1 (x2::'a) x3 x4. (a ∧ x3 ∨ x4 ∧ x1))"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_4:
  shows "(∀x1 x2. (∀x3 . (∀x4. a))) = (∀x1 x2 x3 x4. a)"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_5:
  shows "(∃x1. a) = (∃x1. a)"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_6:
  shows "(∃x1 . (∃x2. a ∧ x1)) = (∃x1 x2. a ∧ x1)"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_7:
  shows "(∃x1 (x2::'a). (∃x3 x4. (a ∧ x3 ∨ x4 ∧ x1))) = (∃x1 (x2::'a) x3 x4. (a ∧ x3 ∨ x4 ∧ x1))"
  by (ctxt_tactic "qnt_join")

lemma qnt_join_8:
  shows "(∃x1 x2. (∃x3 . (∃x4. a))) = (∀x1 x2 x3 x4. a)"
  by (ctxt_tactic "qnt_join")

(* Rule 83: qnt_rm_ununsed *)

lemma qnt_rm_unused_1:
  shows "(∀x1. a) = a"
  by (ctxt_tactic "qnt_rm_unused")

lemma qnt_rm_unused_2:
  shows "(∀x1 x2. x2) = (∀x2. x2)"
  by (ctxt_tactic "qnt_rm_unused")

lemma qnt_rm_unused_3:
  shows "(∀x1 x2 x3. x1 ∧ x3) = (∀x1 x3. x1 ∧ x3)"
  by (ctxt_tactic "qnt_rm_unused")

lemma qnt_rm_unused_4:
  shows "(∃x1. a) = a"
  by (ctxt_tactic "qnt_rm_unused")

lemma qnt_rm_unused_5:
  shows "(∃x1 x2. x2) = (∃x2. x2)"
  by (ctxt_tactic "qnt_rm_unused")

lemma qnt_rm_unused_6:
  shows "(∃x1 x2 x3. x1 ∧ x3) = (∃x1 x3. x1 ∧ x3)"
  by (ctxt_tactic "qnt_rm_unused")

lemma
‹(∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) (v0a::'A_literal_multiset_list__a__i) (v2a::'A_literal_multiset_list__a__i) (v3a::'A_multiset_list__a__i)
             (v4a::'A_list__a__i) (v5a::'A_literal_multiset__a__i) v1a::'Nat__a__i.
             v1a ≠ (size__a__ia::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i) v0a ∨
             v1a ≠ size__a__ia v2a ∨
             v1a ≠ (size__a__i::'A_multiset_list__a__i ⇒ 'Nat__a__i) v3a ∨
             v1a ≠ (size__a__ib::'A_list__a__i ⇒ 'Nat__a__i) v4a ∨
             (zero__a__ib::'Nat__a__i) = v1a ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ (less__a__i::'Nat__a__i ⇒ 'Nat__a__i ⇒ bool) v6 v1a ∨
                    (nth__a__i::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_literal_multiset__a__i) v0a v6 =
                    (plus__a__i::'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) (nth__a__i v2a v6)
                     ((image_mset__a__i::'A_a_literal_fun__a__i ⇒ 'A_multiset__a__i ⇒ 'A_literal_multiset__a__i) (pos__a__i::'A_a_literal_fun__a__i)
                       ((nth__a__ia::'A_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_multiset__a__i) v3a v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1a ∨ (zero__a__i::'A_multiset__a__i) ≠ nth__a__ia v3a v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1a ∨
                    ¬ (member__a__i::'A__a__i ⇒ 'A_set__a__i ⇒ bool) isabelle_internal_BOUND_VARIABLE_7618
                        ((set_mset__a__i::'A_multiset__a__i ⇒ 'A_set__a__i) (nth__a__ia v3a v6)) ∨
                    (nth__a__ib::'A_list__a__i ⇒ 'Nat__a__i ⇒ 'A__a__i) v4a v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ (eligible__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
                 (s__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i) v4a
                 (plus__a__i v5a (image_mset__a__i (neg__a__i::'A_a_literal_fun__a__i) ((mset__a__i::'A_list__a__i ⇒ 'A_multiset__a__i) v4a))) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨ (strictly_maximal_wrt__a__i::'A__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool) (nth__a__ib v4a v6) (nth__a__i v2a v6)) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨
                    (zero__a__ia::'A_literal_multiset__a__i) =
                    (fun_app__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) s__a__i
                     (nth__a__i v0a v6)) ∨
             (ord_resolve__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i
                            ⇒ 'A_literal_multiset_list__a__i
                               ⇒ 'A_literal_multiset__a__i ⇒ 'A_multiset_list__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
              s__a__i v0a (plus__a__i v5a (image_mset__a__i neg__a__i (mset__a__i v4a))) v3a v4a
              (plus__a__i
                ((sum_mset__a__i::'A_literal_multiset_multiset__a__i ⇒ 'A_literal_multiset__a__i)
                  ((mset__a__ia::'A_literal_multiset_list__a__i ⇒ 'A_literal_multiset_multiset__a__i) v2a))
                v5a)) =
         (∀(v0::'A_literal_multiset_list__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) v1::'Nat__a__i.
             v1 ≠ size__a__ia v0 ∨
             v1 ≠ size__a__ia v2 ∨
             v1 ≠ size__a__i v3 ∨
             v1 ≠ size__a__ib v4 ∨
             zero__a__ib = v1 ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ nth__a__i v0 v6 = plus__a__i (nth__a__i v2 v6) (image_mset__a__i pos__a__i (nth__a__ia v3 v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__i ≠ nth__a__ia v3 v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1 ∨
                    ¬ member__a__i isabelle_internal_BOUND_VARIABLE_7618 (set_mset__a__i (nth__a__ia v3 v6)) ∨
                    nth__a__ib v4 v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ eligible__a__i s__a__i v4 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ strictly_maximal_wrt__a__i (nth__a__ib v4 v6) (nth__a__i v2 v6)) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__ia = fun_app__a__i s__a__i (nth__a__i v0 v6)) ∨
             ord_resolve__a__i s__a__i v0 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) v3 v4 (plus__a__i (sum_mset__a__i (mset__a__ia v2)) v5)) ›
  by (ctxt_tactic "qnt_rm_unused")
  
lemma ‹ (∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) (v0a::'A_literal_multiset_list__a__i) (v2a::'A_literal_multiset_list__a__i) (v3a::'A_multiset_list__a__i)
             (v4a::'A_list__a__i) (v5a::'A_literal_multiset__a__i) v1a::'Nat__a__i.
             v1a ≠ (size__a__ia::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i) v0a ∨
             v1a ≠ size__a__ia v2a ∨
             v1a ≠ (size__a__i::'A_multiset_list__a__i ⇒ 'Nat__a__i) v3a ∨
             v1a ≠ (size__a__ib::'A_list__a__i ⇒ 'Nat__a__i) v4a ∨
             (zero__a__ib::'Nat__a__i) = v1a ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ (less__a__i::'Nat__a__i ⇒ 'Nat__a__i ⇒ bool) v6 v1a ∨
                    (nth__a__i::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_literal_multiset__a__i) v0a v6 =
                    (plus__a__i::'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) (nth__a__i v2a v6)
                     ((image_mset__a__i::'A_a_literal_fun__a__i ⇒ 'A_multiset__a__i ⇒ 'A_literal_multiset__a__i) (pos__a__i::'A_a_literal_fun__a__i)
                       ((nth__a__ia::'A_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_multiset__a__i) v3a v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1a ∨ (zero__a__i::'A_multiset__a__i) ≠ nth__a__ia v3a v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1a ∨
                    ¬ (member__a__i::'A__a__i ⇒ 'A_set__a__i ⇒ bool) isabelle_internal_BOUND_VARIABLE_7618
                        ((set_mset__a__i::'A_multiset__a__i ⇒ 'A_set__a__i) (nth__a__ia v3a v6)) ∨
                    (nth__a__ib::'A_list__a__i ⇒ 'Nat__a__i ⇒ 'A__a__i) v4a v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ (eligible__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
                 (s__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i) v4a
                 (plus__a__i v5a (image_mset__a__i (neg__a__i::'A_a_literal_fun__a__i) ((mset__a__i::'A_list__a__i ⇒ 'A_multiset__a__i) v4a))) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨ (strictly_maximal_wrt__a__i::'A__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool) (nth__a__ib v4a v6) (nth__a__i v2a v6)) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨
                    (zero__a__ia::'A_literal_multiset__a__i) =
                    (fun_app__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) s__a__i
                     (nth__a__i v0a v6)) ∨
             (ord_resolve__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i
                            ⇒ 'A_literal_multiset_list__a__i
                               ⇒ 'A_literal_multiset__a__i ⇒ 'A_multiset_list__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
              s__a__i v0a (plus__a__i v5a (image_mset__a__i neg__a__i (mset__a__i v4a))) v3a v4a
              (plus__a__i
                ((sum_mset__a__i::'A_literal_multiset_multiset__a__i ⇒ 'A_literal_multiset__a__i)
                  ((mset__a__ia::'A_literal_multiset_list__a__i ⇒ 'A_literal_multiset_multiset__a__i) v2a))
                v5a)) =
         (∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             v5::'A_literal_multiset__a__i.
             v1 ≠ size__a__ia v0 ∨
             v1 ≠ size__a__ia v2 ∨
             v1 ≠ size__a__i v3 ∨
             v1 ≠ size__a__ib v4 ∨
             zero__a__ib = v1 ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ nth__a__i v0 v6 = plus__a__i (nth__a__i v2 v6) (image_mset__a__i pos__a__i (nth__a__ia v3 v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__i ≠ nth__a__ia v3 v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1 ∨
                    ¬ member__a__i isabelle_internal_BOUND_VARIABLE_7618 (set_mset__a__i (nth__a__ia v3 v6)) ∨
                    nth__a__ib v4 v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ eligible__a__i s__a__i v4 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ strictly_maximal_wrt__a__i (nth__a__ib v4 v6) (nth__a__i v2 v6)) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__ia = fun_app__a__i s__a__i (nth__a__i v0 v6)) ∨
             ord_resolve__a__i s__a__i v0 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) v3 v4 (plus__a__i (sum_mset__a__i (mset__a__ia v2)) v5)) ›
  by (ctxt_tactic "qnt_rm_unused")

lemma ‹(∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) (v0a::'A_literal_multiset_list__a__i) (v2a::'A_literal_multiset_list__a__i) (v3a::'A_multiset_list__a__i)
             (v4a::'A_list__a__i) (v5a::'A_literal_multiset__a__i) v1a::'Nat__a__i.
             v1a ≠ (size__a__ia::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i) v0a ∨
             v1a ≠ size__a__ia v2a ∨
             v1a ≠ (size__a__i::'A_multiset_list__a__i ⇒ 'Nat__a__i) v3a ∨
             v1a ≠ (size__a__ib::'A_list__a__i ⇒ 'Nat__a__i) v4a ∨
             (zero__a__ib::'Nat__a__i) = v1a ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ (less__a__i::'Nat__a__i ⇒ 'Nat__a__i ⇒ bool) v6 v1a ∨
                    (nth__a__i::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_literal_multiset__a__i) v0a v6 =
                    (plus__a__i::'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) (nth__a__i v2a v6)
                     ((image_mset__a__i::'A_a_literal_fun__a__i ⇒ 'A_multiset__a__i ⇒ 'A_literal_multiset__a__i) (pos__a__i::'A_a_literal_fun__a__i)
                       ((nth__a__ia::'A_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_multiset__a__i) v3a v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1a ∨ (zero__a__i::'A_multiset__a__i) ≠ nth__a__ia v3a v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1a ∨
                    ¬ (member__a__i::'A__a__i ⇒ 'A_set__a__i ⇒ bool) isabelle_internal_BOUND_VARIABLE_7618
                        ((set_mset__a__i::'A_multiset__a__i ⇒ 'A_set__a__i) (nth__a__ia v3a v6)) ∨
                    (nth__a__ib::'A_list__a__i ⇒ 'Nat__a__i ⇒ 'A__a__i) v4a v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ (eligible__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
                 (s__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i) v4a
                 (plus__a__i v5a (image_mset__a__i (neg__a__i::'A_a_literal_fun__a__i) ((mset__a__i::'A_list__a__i ⇒ 'A_multiset__a__i) v4a))) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨ (strictly_maximal_wrt__a__i::'A__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool) (nth__a__ib v4a v6) (nth__a__i v2a v6)) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨
                    (zero__a__ia::'A_literal_multiset__a__i) =
                    (fun_app__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) s__a__i
                     (nth__a__i v0a v6)) ∨
             (ord_resolve__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i
                            ⇒ 'A_literal_multiset_list__a__i
                               ⇒ 'A_literal_multiset__a__i ⇒ 'A_multiset_list__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
              s__a__i v0a (plus__a__i v5a (image_mset__a__i neg__a__i (mset__a__i v4a))) v3a v4a
              (plus__a__i
                ((sum_mset__a__i::'A_literal_multiset_multiset__a__i ⇒ 'A_literal_multiset__a__i)
                  ((mset__a__ia::'A_literal_multiset_list__a__i ⇒ 'A_literal_multiset_multiset__a__i) v2a))
                v5a)) =
         (∀(v0::'A_literal_multiset_list__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) v1::'Nat__a__i.
             v1 ≠ size__a__ia v0 ∨
             v1 ≠ size__a__ia v2 ∨
             v1 ≠ size__a__i v3 ∨
             v1 ≠ size__a__ib v4 ∨
             zero__a__ib = v1 ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ nth__a__i v0 v6 = plus__a__i (nth__a__i v2 v6) (image_mset__a__i pos__a__i (nth__a__ia v3 v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__i ≠ nth__a__ia v3 v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1 ∨
                    ¬ member__a__i isabelle_internal_BOUND_VARIABLE_7618 (set_mset__a__i (nth__a__ia v3 v6)) ∨
                    nth__a__ib v4 v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ eligible__a__i s__a__i v4 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ strictly_maximal_wrt__a__i (nth__a__ib v4 v6) (nth__a__i v2 v6)) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__ia = fun_app__a__i s__a__i (nth__a__i v0 v6)) ∨
             ord_resolve__a__i s__a__i v0 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) v3 v4 (plus__a__i (sum_mset__a__i (mset__a__ia v2)) v5)) ›
  by (ctxt_tactic "qnt_rm_unused")
lemma ‹(∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             (v5::'A_literal_multiset__a__i) (v0a::'A_literal_multiset_list__a__i) (v2a::'A_literal_multiset_list__a__i) (v3a::'A_multiset_list__a__i)
             (v4a::'A_list__a__i) (v5a::'A_literal_multiset__a__i) v1a::'Nat__a__i.
             v1a ≠ (size__a__ia::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i) v0a ∨
             v1a ≠ size__a__ia v2a ∨
             v1a ≠ (size__a__i::'A_multiset_list__a__i ⇒ 'Nat__a__i) v3a ∨
             v1a ≠ (size__a__ib::'A_list__a__i ⇒ 'Nat__a__i) v4a ∨
             (zero__a__ib::'Nat__a__i) = v1a ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ (less__a__i::'Nat__a__i ⇒ 'Nat__a__i ⇒ bool) v6 v1a ∨
                    (nth__a__i::'A_literal_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_literal_multiset__a__i) v0a v6 =
                    (plus__a__i::'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) (nth__a__i v2a v6)
                     ((image_mset__a__i::'A_a_literal_fun__a__i ⇒ 'A_multiset__a__i ⇒ 'A_literal_multiset__a__i) (pos__a__i::'A_a_literal_fun__a__i)
                       ((nth__a__ia::'A_multiset_list__a__i ⇒ 'Nat__a__i ⇒ 'A_multiset__a__i) v3a v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1a ∨ (zero__a__i::'A_multiset__a__i) ≠ nth__a__ia v3a v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1a ∨
                    ¬ (member__a__i::'A__a__i ⇒ 'A_set__a__i ⇒ bool) isabelle_internal_BOUND_VARIABLE_7618
                        ((set_mset__a__i::'A_multiset__a__i ⇒ 'A_set__a__i) (nth__a__ia v3a v6)) ∨
                    (nth__a__ib::'A_list__a__i ⇒ 'Nat__a__i ⇒ 'A__a__i) v4a v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ (eligible__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
                 (s__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i) v4a
                 (plus__a__i v5a (image_mset__a__i (neg__a__i::'A_a_literal_fun__a__i) ((mset__a__i::'A_list__a__i ⇒ 'A_multiset__a__i) v4a))) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨ (strictly_maximal_wrt__a__i::'A__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool) (nth__a__ib v4a v6) (nth__a__i v2a v6)) ∨
             ¬ (∀v6::'Nat__a__i.
                    ¬ less__a__i v6 v1a ∨
                    (zero__a__ia::'A_literal_multiset__a__i) =
                    (fun_app__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i ⇒ 'A_literal_multiset__a__i ⇒ 'A_literal_multiset__a__i) s__a__i
                     (nth__a__i v0a v6)) ∨
             (ord_resolve__a__i::'A_literal_multiset_a_literal_multiset_fun__a__i
                            ⇒ 'A_literal_multiset_list__a__i
                               ⇒ 'A_literal_multiset__a__i ⇒ 'A_multiset_list__a__i ⇒ 'A_list__a__i ⇒ 'A_literal_multiset__a__i ⇒ bool)
              s__a__i v0a (plus__a__i v5a (image_mset__a__i neg__a__i (mset__a__i v4a))) v3a v4a
              (plus__a__i
                ((sum_mset__a__i::'A_literal_multiset_multiset__a__i ⇒ 'A_literal_multiset__a__i)
                  ((mset__a__ia::'A_literal_multiset_list__a__i ⇒ 'A_literal_multiset_multiset__a__i) v2a))
                v5a)) =
         (∀(v0::'A_literal_multiset_list__a__i) (v1::'Nat__a__i) (v2::'A_literal_multiset_list__a__i) (v3::'A_multiset_list__a__i) (v4::'A_list__a__i)
             v5::'A_literal_multiset__a__i.
             v1 ≠ size__a__ia v0 ∨
             v1 ≠ size__a__ia v2 ∨
             v1 ≠ size__a__i v3 ∨
             v1 ≠ size__a__ib v4 ∨
             zero__a__ib = v1 ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ nth__a__i v0 v6 = plus__a__i (nth__a__i v2 v6) (image_mset__a__i pos__a__i (nth__a__ia v3 v6))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__i ≠ nth__a__ia v3 v6) ∨
             ¬ (∀(v6::'Nat__a__i) isabelle_internal_BOUND_VARIABLE_7618::'A__a__i.
                    ¬ less__a__i v6 v1 ∨
                    ¬ member__a__i isabelle_internal_BOUND_VARIABLE_7618 (set_mset__a__i (nth__a__ia v3 v6)) ∨
                    nth__a__ib v4 v6 = isabelle_internal_BOUND_VARIABLE_7618) ∨
             ¬ eligible__a__i s__a__i v4 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ strictly_maximal_wrt__a__i (nth__a__ib v4 v6) (nth__a__i v2 v6)) ∨
             ¬ (∀v6::'Nat__a__i. ¬ less__a__i v6 v1 ∨ zero__a__ia = fun_app__a__i s__a__i (nth__a__i v0 v6)) ∨
             ord_resolve__a__i s__a__i v0 (plus__a__i v5 (image_mset__a__i neg__a__i (mset__a__i v4))) v3 v4 (plus__a__i (sum_mset__a__i (mset__a__ia v2)) v5)) ›
  supply [[show_types=false]]
  by (ctxt_tactic "qnt_rm_unused")

(* Rule 83: eq_simplify *)

lemma eq_simplify_1:
  shows "(a = a) = True"
  by (ctxt_tactic "eq_simplify")

lemma eq_simplify_2:
  shows "((3::int) = 3) = True"
  by (ctxt_tactic "eq_simplify")

lemma eq_simplify_3:
  shows "((3::int) = 4) = False"
  by (ctxt_tactic "eq_simplify")

lemma eq_simplify_4:
  shows "¬((3::int) = 3) = False"
  by (ctxt_tactic "eq_simplify")

lemma eq_simplify_5:
  shows "((0:: int) = -1) = False"
  by (ctxt_tactic "eq_simplify")

lemma eq_simplify_6:
  shows "(-1 = (0:: int)) = False"
  by (ctxt_tactic "eq_simplify")

(* Rule 85: div_simplify *)

lemma div_simplify_1:
  shows "((3::int) = 3) = True"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_2:
  shows "((3::int) = 4) = False"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_2b:
  shows "((-3::int) = 4) = False"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_3:
  shows "((3::int) div 3) = 1"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_3b:
  shows "((-3::int) div 3) = -1"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_3c:
  shows "((-3::int) div -3) = 1"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4a:
  shows "((-20::int) div -3) = 6"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4b:
  shows "((-21::int) div -3) = 7"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4c:
  shows "(((178::int) div -3) = 7) = False"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4d:
  shows "(((179::int) div -3) = 7000) = False"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4e:
  shows "(((82388::int) div -3) = 7000) = False"
  by (ctxt_tactic "div_simplify")

lemma div_simplify_4f:
  shows "(((82388::int) div -30000) = 7000) = False"
  by (ctxt_tactic "div_simplify")

(* Rule 86: prod_simplify *)

lemma prod_simplify_1:
  shows "(3 * 4 * 5) = (60::int)"
  by (ctxt_tactic "prod_simplify")

lemma prod_simplify_2:
  shows "(3 * 4 * 0 * x) = (0::int)"
  by (ctxt_tactic "prod_simplify")

lemma prod_simplify_3:
  shows "(3 * y * 4 * 2 * x * 5) = (120::int) * y * x"
  by (ctxt_tactic "prod_simplify")

lemma prod_simplify_4:
  shows "(1 * y * 1 * x) = (y::int) * x"
  by (ctxt_tactic "prod_simplify")

lemma prod_simplify_5:
  shows "(13 + (1 * y * 0 * x)) = (13::int) + 0"
  by (ctxt_tactic "prod_simplify")

lemma prod_simplify_6:
  shows "(2 * (2 * y * 3 * x) * 1) = (12::int) * y * x"
  by (ctxt_tactic "prod_simplify")

(* Rule 87: unary_minus_simplify *)

lemma unary_minus_simplify_1:
  shows "- (-(3 * 4 * 5)) = ((3::int) * 4 * 5)"
  by (ctxt_tactic "unary_minus_simplify")

lemma unary_minus_simplify_2:
  shows "- (-3) = (3::int)"
  by (ctxt_tactic "unary_minus_simplify")

lemma unary_minus_simplify_3:
  shows "- (- (-3)) = -(3::int)"
  by (ctxt_tactic "unary_minus_simplify")

(* Rule 88: minus_simplify *)

lemma minus_simplify_1:
  shows "x - x = (0::int)"
  by (ctxt_tactic "minus_simplify")

lemma minus_simplify_2:
  shows "x - 0 = (x::int)"
  by (ctxt_tactic "minus_simplify")

lemma minus_simplify_3:
  shows "x - 0 - x = (0::int)"
  by (ctxt_tactic "minus_simplify")

lemma minus_simplify_4:
  shows "0 - x - 0 - (-2 - 3) = -(x::int) - -5"
  by (ctxt_tactic "minus_simplify")

(* Rule 89: sum_simplify *)

lemma sum_simplify_1:
  shows "1 + 3 + 22 = (26::int)"
  by (ctxt_tactic "sum_simplify")

lemma sum_simplify_2:
  shows "1 + 3 + -4 = (0::int)"
  by (ctxt_tactic "sum_simplify")

lemma sum_simplify_3:
  shows "1 + 3 + x + -4 + (y + 0) = (0::int) + x + y"
  by (ctxt_tactic "sum_simplify")

(* Rule 90: comp_simplify *)

lemma comp_simplify_1:
  shows "(2 < (3::int)) = True"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_2:
  shows "(2 < (1::int)) = False"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_3:
  shows "(2 ≤ (3::int)) = True"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_4:
  shows "(2 ≤ (1::int)) = False"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_5:
  shows "(2 < (2::int)) = False"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_6:
  shows "(2 ≤ (2::int)) = True"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_7:
  shows "(5 ≥ (2::int)) = ((2::int) ≤ 5)"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_8:
  shows "(3 < (12::int)) = (¬((12::int) ≤ 3))"
  by (ctxt_tactic "comp_simplify")

lemma comp_simplify_9:
  shows "(55 > (7::int)) = (¬((55::int) ≤ 7))"
  by (ctxt_tactic "comp_simplify")

(* Rule 93: distinct_elim *)

lemma distinct_elim_1: "(x ≠ y) = (x ≠ y)"
  by (ctxt_tactic "distinct_elim")

lemma distinct_elim_2: "(((x::bool) ≠ y) ∧ ((x::bool) ≠ z) ∧ ((y::bool) ≠ z)) = False"
  by (ctxt_tactic "distinct_elim")

lemma distinct_elim_3: "(((x::int) ≠ y) ∧ ((x::int) ≠ z) ∧ ((y::int) ≠ z)) = (((x::int) ≠ y) ∧ ((x::int) ≠ z) ∧ ((y::int) ≠ z))"
  by (ctxt_tactic "distinct_elim")

lemma distinct_elim_4: "(((x::bool) ≠ y) ∧ ((x::bool) ≠ z) ∧ ((x::bool) ≠ a) ∧ ((y::bool) ≠ z) ∧ ((y::bool) ≠ a) ∧ ((z::bool) ≠ a)) = False"
  by (ctxt_tactic "distinct_elim")

lemma distinct_elim_5:
  "(((x::bool) ≠ y) ∧ ((x::bool) ≠ z) ∧ ((x::bool) ≠ a) ∧ ((x::bool) ≠ b)
 ∧ ((y::bool) ≠ z) ∧ ((y::bool) ≠ a) ∧ ((y::bool) ≠ b)
 ∧ ((z::bool) ≠ a) ∧ ((z::bool) ≠ b)
 ∧ ((a::bool) ≠ b)
 ) = False"
  by (ctxt_tactic "distinct_elim")

lemma distinct_elim_6:
  "(((x::bool) ≠ y) ∧ ((x::bool) ≠ z) ∧ ((x::bool) ≠ a) ∧ ((x::bool) ≠ b) ∧ ((x::bool) ≠ c)
 ∧ ((y::bool) ≠ z) ∧ ((y::bool) ≠ a) ∧ ((y::bool) ≠ b) ∧ ((y::bool) ≠ c)
 ∧ ((z::bool) ≠ a) ∧ ((z::bool) ≠ b) ∧ ((z::bool) ≠ c)
 ∧ ((a::bool) ≠ b) ∧ ((a::bool) ≠ c)
 ∧ ((b::bool) ≠ c)
 ) = False"
  by (ctxt_tactic "distinct_elim")

(* Rule 94: la_rw_eq1 *)

lemma la_rw_eq1_1:
  "(t = (u::int)) = (t ≤ u ∧ u ≤ t)"
  by (ctxt_tactic "la_rw_eq1")

lemma la_rw_eq1_2:
  "(5 = (5::int)) = (5 ≤ (5::int) ∧ 5 ≤ (5::int))"
  by (ctxt_tactic "la_rw_eq1")

lemma la_rw_eq1_3:
  "((7-2) = (5::int)) = ((7-2) ≤ (5::int) ∧ (5::int) ≤ (7-2))"
  by (ctxt_tactic "la_rw_eq1")

(* Rule 95: nary_elim *)

(* Parsing already binarizes and breaks up chains so these are basically equalities  *)

(* left-assoc *)


(* chainable operators are already transformed during parsing *)

lemma nary_elim_1:
  "(t1 = t2 ∧ t2 = t3 ∧ t3 = t4) = (t1 = t2 ∧ t2 = t3 ∧ t3 = t4)"
  by (ctxt_tactic "nary_elim")

lemma nary_elim_2:
  "(t1 = t2) = (t1 = t2)"
  by (ctxt_tactic "nary_elim")

(* Rule 96: bfun_elim *)
(*TODO Pascal: Try and improve tactic to solve these *)
(* Note: This rule is veriT only *)
lemma bfun_elim_1:
  assumes   "∀v0 v1 v2.
            fun_app_b (fun_app_c (fun_app_d (follow delta) v0) v1) v2 =
            (∃v3 v4 v5 v6 v7 v8 v9 v10 v11.
                v0 = fun_app_bg (sCons_j v8) v11 ∧
                v1 = fun_app_bi (sCons_k v7) v4 ∧
                v2 = sCons_d (fun_app_ag (fun_app_t pair_d v9) v10) v6 ∧
                v3 = shd_c v4 ∧
                v5 = fun_app_m fst_a (shd_a v6) ∧
                member (fun_app_w (fun_app_p pair_b v7) (fun_app_ad (fun_app_r pair_c v8) v3)) (fun_app_dy (fun_app_dz (fun_app_ea delta v9) v10) v5) ∧
                fun_app_b (fun_app_c (fun_app_d (follow delta) v11) v4) v6)"
  shows "∀v0 v1 v2.
            fun_app_b (fun_app_c (fun_app_d (follow delta) v0) v1) v2 =
            (∃v3 v4 v5 v6 v7 v9 v10 v11.
                v0 = fun_app_bg (sCons_j False) v11 ∧
                v1 = fun_app_bi (sCons_k v7) v4 ∧
                v2 = sCons_d (fun_app_ag (fun_app_t pair_d v9) v10) v6 ∧
                v3 = shd_c v4 ∧
                v5 = fun_app_m fst_a (shd_a v6) ∧
                member (fun_app_w (fun_app_p pair_b v7) (fun_app_ad (fun_app_r pair_c False) v3)) (fun_app_dy (fun_app_dz (fun_app_ea delta v9) v10) v5) ∧
                fun_app_b (fun_app_c (fun_app_d (follow delta) v11) v4) v6 ∨
                v0 = fun_app_bg (sCons_j True) v11 ∧
                v1 = fun_app_bi (sCons_k v7) v4 ∧
                v2 = sCons_d (fun_app_ag (fun_app_t pair_d v9) v10) v6 ∧
                v3 = shd_c v4 ∧
                v5 = fun_app_m fst_a (shd_a v6) ∧
                member (fun_app_w (fun_app_p pair_b v7) (fun_app_ad (fun_app_r pair_c True) v3)) (fun_app_dy (fun_app_dz (fun_app_ea delta v9) v10) v5) ∧
                fun_app_b (fun_app_c (fun_app_d (follow delta) v11) v4) v6)"
  using assms by (ctxt_tactic "bfun_elim")

(* Rule 97: ite_intro *)
(* Note: This rule is veriT only *)
lemma ite_intro_1: "(If p a b) = ((If p a b) ∧ (If p (a = (If p a b)) (b = (If p a b))))"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_2: "(¬(If p a b)) = ((¬(If p a b)) ∧ (If p (a = (If p a b)) (b = (If p a b))))"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_3: "((If p a b) ∨ (If q c d)) = ( ((If p a b) ∨ (If q c d)) 
                                                 ∧ (If p (a = (If p a b)) (b = (If p a b))) 
                                                 ∧ (If q (c = (If q c d)) (d = (If q c d))) )"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_4: "((If p a b) ∨ ((If q c d) ∧ (If (¬p) b (¬d)))) 
                          = ( ((If p a b) ∨ ((If q c d) ∧ (If (¬p) b (¬d))))
                             ∧ (If p (a = (If p a b)) (b = (If p a b)))
                             ∧ (If q (c = (If q c d)) (d = (If q c d)))
                             ∧ (If (¬p) (b = (If (¬p) b (¬d))) ((¬d) = (If (¬p) b (¬d)))) )"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_5: "(a ∨ b) = (a ∨ b)"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_6: "(If p a b) = (If p a b)"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_7: "((If p a b) ∧ ((If q c d) ∨ (If (¬p) b (~d)))) 
                    = ((If p a b) ∧ ((If q c d) ∨ (If (¬p) b (~d))))"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_8: "((If p a b) ∨ (If q c d) ∨ (If q d a)) 
                          = ( (((If p a b) ∨ (If q c d) ∨ (If q d a)))
                              ∧ (If p (a = (If p a b)) (b = (If p a b)))
                              ∧ (If q (d = (If q d a)) (a = (If q d a))) )"
  by (ctxt_tactic "ite_intro")

lemma ite_intro_9:
  fixes dec_10 :: ‹int ⇒ int›
  shows
  ‹ (dec_10 (4 * dec_10 4) = (if 4 * dec_10 4 < 10 then 4 * dec_10 4 else dec_10 (4 * dec_10 4 - 10))) =
         (dec_10 (4 * dec_10 4) = (if 4 * dec_10 4 < 10 then 4 * dec_10 4 else dec_10 (4 * dec_10 4 - 10)) ∧
          (if 4 * dec_10 4 < 10 then 4 * dec_10 4 = (if 4 * dec_10 4 < 10 then 4 * dec_10 4 else dec_10 (4 * dec_10 4 - 10))
           else dec_10 (4 * dec_10 4 - 10) = (if 4 * dec_10 4 < 10 then 4 * dec_10 4 else dec_10 (4 * dec_10 4 - 10)))) ›
  by (ctxt_tactic "ite_intro")

lemma ite_intro_10:
  shows ‹((if t < 0 then - t else t) = cmod (complex_of_real t)) =
         (cmod (complex_of_real t) = (if t < 0 then - t else t) ∧ 
     (if t < 0 then - t = (if t < 0 then - t else t) else t = (if t < 0 then - t else t)))›
  by (ctxt_tactic "ite_intro")

(* Rule 104: miniscope_distribute *)
(*Note: there isn't a solver that produces the exists case currently*)

lemma miniscope_distribute_all1:
  "(∀x1::'a. a) = (∀x1::'a. a)"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_all2:
  "(∀x1::'a. (a ∧ b)) = ((∀x1::'a. a) ∧ (∀x1::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_all3:
  "(∀x1::'a. (a ∧ (b ∧ c))) = ((∀x1::'a. a) ∧ (∀x1::'a. b) ∧ (∀x1::'a. c))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_all4:
  "(∀x1 ::'a. ∀ x2 ::'a. (a ∧ b)) = ((∀x1::'a. ∀x2::'a. a) ∧ (∀x1::'a. ∀x2::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_all5:
  "(∀x1::'a. ((x1 = a) ∧ b)) = ((∀x1::'a. x1 = a) ∧ (∀x1::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_ex1:
  "(∃x1::'a. a) = (∃x1::'a. a)"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_ex2:
  "(∃x1::'a. (a ∨ b)) = ((∃x1::'a. a) ∨ (∃x1::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_ex3:
  "(∃x1::'a. (a ∨ (b ∨ c))) = ((∃x1::'a. a) ∨ (∃x1::'a. b) ∨ (∃x1::'a. c))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_ex4:
  "(∃x1::'a. ∃x2 ::'a. (a ∨ b)) = ((∃x1::'a. ∃x2::'a. a) ∨ (∃x1::'a. ∃x2::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

lemma miniscope_distribute_ex5:
  "(∃x1::'a. ((x1 = a) ∨ b)) = ((∃x1::'a. x1 = a) ∨ (∃x1::'a. b))"
  by (ctxt_tactic "miniscope_distribute")

(* Rule 105: miniscope_split *)
(*Note: there isn't a solver that produces the exists case currently*)

lemma miniscope_split_all1:
  "(∀x1::'a. a) = (∀x1::'a. a)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all2:
  "(∀x1::'a. (a ∨ b)) = ((∀x1::'a. a) ∨ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all3:
  "(∀x1::'a. ∀x2::'a. (a ∨ (b ∨ c))) = ((∀x1::'a. a) ∨ b ∨ (∀x2::'a. c))"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all4:
  "(∀x1::'a. ∀x2::'a. (a ∨ b)) = ((∀x1::'a. ∀x2::'a. a) ∨ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all5:
  "(∀x1::'a. ∀x2::'a. (a ∨ b)) = (a ∨ (∀x1::'a. ∀x2::'a. b))"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all6:
  "(∀x1::'a. ((x1 = a) ∨ b)) = ((∀x1::'a. x1 = a) ∨ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_all7:
  "(∀x1 ::'a. ∀x2 ::'a. (a ∨ b)) = ((∀x2::'a. a) ∨ (∀x1::'a. b))"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex1:
  "(∃x1::'a. a) = (∃x1::'a. a)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex2:
  "(∃x1::'a. (a ∧ b)) = ((∃x1::'a. a) ∧ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex3:
  "(∃x1 x2::'a. (a ∧ (b ∧ c))) = ((∃x1::'a. a) ∧ b ∧ (∃x2::'a. c))"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex4:
  "(∃x1 ::'a. ∃x2 ::'a. (a ∧ b)) = ((∃x1::'a. ∃x2::'a. a) ∧ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex5:
  "(∃x1 ::'a. ∃x2 ::'a. (a ∧ b)) = (a ∧ (∃x1::'a. ∃x2::'a. b))"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex6:
  "(∃x1::'a. ((x1 = a) ∧ b)) = ((∃x1::'a. x1 = a) ∧ b)"
  by (ctxt_tactic "miniscope_split")

lemma miniscope_split_ex7:
  "(∃x1 ::'a. ∃x2 ::'a. (a ∧ b)) = ((∃x2::'a. a) ∧ (∃x1::'a. b))"
  by (ctxt_tactic "miniscope_split")

(* Rule 106: miniscope_ite *)

lemma miniscope_split_ite1:
  "(∀x1 ::'a. ∀x2 ::'a. (If a b c)) = (If a (∀x1 ::'a. ∀x2 ::'a. b) (∀x1 ::'a. ∀x2 ::'a. c))"
  by (ctxt_tactic "miniscope_ite")

lemma miniscope_split_ite2:
  "(∀x1 ::'a. ∀x2 ::'a. (If a (P1 x1) (P2 x2))) = (If a (∀x1 ::'a. ∀x2 ::'a. P1 x1) (∀x1 ::'a. ∀x2 ::'a. P2 x2))"
  by (ctxt_tactic "miniscope_ite")

(* Rule 106: miniscope_or *)

lemma miniscope_or1:
"(∀y. (n ≠ r m n ∨ a ∨¬ f m n y y ∨ n = y)) = ((n ≠ r m n) ∨ a ∨(∀y. (¬ f m n y y ∨ n = y)))"
  by (ctxt_tactic "miniscope_or")

(*Rule : poly_simp_rel*)

lemma poly_simp_rel1:
  assumes "- 1  *  ((arg2::int) + (2::int) * (x::int) + - 1 * (mul2_sum::int) - 1) =
         - 1  * ( (arg2 + (2::int) * x + - 1 * mul2_sum) -  1)"
  shows "((arg2::int) + (2::int) * (x::int) + - 1 * (mul2_sum::int) < 1) =
         ( (arg2 + (2::int) * x + - 1 * mul2_sum) <  1)"
  using assms
  by (ctxt_tactic "poly_simp_rel")

lemma poly_simp_rel2:
  assumes "-88  *  ((arg2::int) + (2::int) * (x::int) + - 1 * (mul2_sum::int) - 1) =
        - 15  * ( (arg2 + (2::int) * x + - 1 * mul2_sum) -  1)"
  shows "((arg2::int) + (2::int) * (x::int) + - 1 * (mul2_sum::int) < 1) =
         ( (arg2 + (2::int) * x + - 1 * mul2_sum) <  1)"
  using assms
  by (ctxt_tactic "poly_simp_rel")


lemma ‹(lift_x::int) + (3::int) = (3::int) + lift_x›
  by (ctxt_tactic "poly_simp")

(*onepoint**)
experiment
begin

context
  fixes v0 :: ‹'a :: {one}›
  assumes H: ‹v0 = 1›
begin

lemma H: ‹(v0 ≠ 1 ∨ v0 ≠ 1) = (1 ≠ 1)›
  using H by blast

end

ML ‹
Alethe_Replay_Methods.onepoint @{context} @{thms H[where 'a=nat]}
  @{term ‹Trueprop ((∀v0::nat. (v0 ≠ 1 ∨ v0 ≠ 1)) = ((1::nat) ≠ 1))›}
|> Thm.prop_of
|> curry (op =) @{term ‹Trueprop ((∀v0::nat. (v0 ≠ 1 ∨ v0 ≠ 1)) = ((1::nat) ≠ 1))›}
|> (fn x => if not x then error "failed" else ())›
end


context
  fixes
LIM :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ bool"
    (‹(‹notation=‹infix LIM››(_)/ ─(_)/→ (_))› [60, 0, 60] 60)
begin


context
  fixes v0 v1 :: ‹'a› and v4 v5 :: 'b
  assumes H: ‹v0 = v1› ‹v4 = v5›
begin
lemma H:
 ‹(v0 = v1 ∧ (∀v6. v1 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v5 ⟶ v2 ─v0→ v4 = v3 ─v1→ v5) =
         (v0 = v0 ∧ (∀v6. v0 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v4 ⟶ v2 ─v0→ v4 = v3 ─v0→ v4)›
  using H by auto
end

ML ‹
Alethe_Replay_Methods.onepoint @{context} @{thms H}
  @{term ‹Trueprop ((∀v0 v1 v2 v3 v4 v5. v0 = v1 ∧ (∀v6. v1 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v5 ⟶ v2 ─v0→ v4 = v3 ─v1→ v5) =
         (∀v0 v2 v3 v4. v0 = v0 ∧ (∀v6. v0 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v4 ⟶ v2 ─v0→ v4 = v3 ─v0→ v4))›}
|> @{print}
|> Thm.prop_of
|> curry (op =) @{term ‹Trueprop ((∀(v0::'a) (v1::'a) (v2::'a ⇒ 'b) (v3::'a ⇒ 'b) (v4::'b) v5::'b. v0 = v1 ∧ (∀v6::'a. v1 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v5 ⟶ v2 ─v0→ v4 = v3 ─v1→ v5) =
 (∀(v0::'a) (v2::'a ⇒ 'b) (v3::'a ⇒ 'b) v4::'b. v0 = v0 ∧ (∀v6::'a. v0 ≠ v6 ⟶ v2 v6 = v3 v6) ∧ v4 = v4 ⟶ v2 ─v0→ v4 = v3 ─v0→ v4))›}
|> (fn x => if not x then error "failed" else ())›

end


experiment
begin

context
  fixes v1 :: nat
begin

context
  fixes v0 :: ‹nat›
begin

lemma H: ‹(v0 ≠ 0 ∨ v0 ≠ 0 ∨ v1 ≠ 1 ∨ v0 ≠ v1) = (0 ≠ 0 ∨ v1 ≠ 1 ∨ 0 ≠ v1)›
  by auto

end

ML ‹
Alethe_Replay_Methods.onepoint @{context} @{thms H}
  @{term ‹Trueprop ((∀v0. v0 ≠ 0 ∨ v0 ≠ 0 ∨ v1 ≠ 1 ∨ v0 ≠ v1) = (0 ≠ (0::nat) ∨ v1 ≠ 1 ∨ 0 ≠ v1))›}
|> @{print}
|> Thm.prop_of
|> curry (op =) @{term ‹Trueprop ((∀v0::nat. v0 ≠ 0 ∨ v0 ≠ 0 ∨ v1 ≠ 1 ∨ v0 ≠ v1) = (0 ≠ (0::nat) ∨ v1 ≠ 1 ∨ 0 ≠ v1))›}
|> (fn x => if not x then error "failed" else ())›

end

end

experiment
begin

context
    fixes A:: "('a ⇒ 'a) set" and result_lub :: "'a set ⇒ 'a"
begin

context
  fixes v0 v1 :: 'a
  assumes H: ‹v1 = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0}›
begin

lemma H: ‹(v1 = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ⟶ v1 = NT ∨ v1 ∈ {uua. ∃xa. xa ∈ A ∧ uua = xa v0}) =
         (result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ⟶
          NT = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ∨ result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ∈ {uua. ∃xa. xa ∈ A ∧ uua = xa v0})›
  using H by auto

end

ML ‹
let
  val goal = @{term ‹Trueprop ((∀v0 v1. v1 = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ⟶ v1 = NT ∨ v1 ∈ {uua. ∃xa. xa ∈ A ∧ uua = xa v0}) =
         (∀v0. result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ⟶
               NT = result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ∨ result_lub {uua. ∃xa. xa ∈ A ∧ uua = xa v0} ∈ {uua. ∃xa. xa ∈ A ∧ uua = xa v0}) )›}
in
Alethe_Replay_Methods.onepoint @{context} @{thms H} goal
|> @{print}
|> Thm.prop_of
|> curry (op =) goal
|> (fn x => if not x then error "failed" else ())
end›

end
end

(* Bind *)
experiment
begin

context
  fixes eq :: "'qt1 ⇒ 'qt1 ⇒ bool" (infix "#=" 50) and
        card_of :: "'var set ⇒ 'var rel" (‹(‹open_block notation=‹mixfix card_of››|_|)›) and
        ordLess2 :: "'var rel ⇒ 'var rel ⇒ bool" (infix ‹<o› 50) and
        qGood :: "'qt1 ⇒ bool" and
        asTerm :: "'qt1 ⇒ 'qt1 set" and
     qrho qrho' :: ‹'qt1 ⇒ 'qt1 ⇒ 'qt1 option› and
     veriT_vr45 veriT_vr50 :: 'qt1
  assumes overall_assms:
    "veriT_vr45 = veriT_vr50"
begin
context
  fixes veriT_vr48' veriT_vr48 veriT_vr47 veriT_vr46 veriT_vr52 
    veriT_vr53 :: 'qt1
  assumes H:
         "veriT_vr46 = veriT_vr52"
         "veriT_vr47 = veriT_vr48'"
         "veriT_vr48 = veriT_vr53"
begin

lemma H: ‹(qrho veriT_vr45 veriT_vr46 = Some veriT_vr47 ∧ qrho' veriT_vr45 veriT_vr46 = Some veriT_vr48 ⟶ veriT_vr47 #= veriT_vr48) =
         (Some veriT_vr48' = qrho veriT_vr50 veriT_vr52 ∧ qrho' veriT_vr50 veriT_vr52 = Some veriT_vr53 ⟶ veriT_vr48' #= veriT_vr53)›
  unfolding H overall_assms by auto

end


lemma ‹(P = Q) ⟹ P = P' ⟹ Q = Q' ⟹ Q = Q'›
  by auto

ML ‹Alethe_Replay_Methods.bind›
ML ‹
let
  val goal = @{term ‹Trueprop ((∀veriT_vr46 veriT_vr47 veriT_vr48. qrho veriT_vr45 veriT_vr46 = Some veriT_vr47 ∧ qrho' veriT_vr45 veriT_vr46 = Some veriT_vr48 ⟶ veriT_vr47 #= veriT_vr48) =
         (∀veriT_vr52 veriT_vr48 veriT_vr53. Some veriT_vr48 = qrho veriT_vr50 veriT_vr52 ∧ qrho' veriT_vr50 veriT_vr52 = Some veriT_vr53 ⟶ veriT_vr48 #= veriT_vr53)  )›}
in
Alethe_Replay_Methods.bind @{context} @{thms H} [
@{term ‹Trueprop (veriT_vr52 = veriT_vr48)›},
@{term ‹Trueprop (veriT_vr48')›},
@{term ‹Trueprop (veriT_vr53)›},
@{term ‹Trueprop (veriT_vr46 = veriT_vr52)›},
@{term ‹Trueprop (veriT_vr47 = veriT_vr48)›},
@{term ‹Trueprop (veriT_vr48' = veriT_vr53)›}]

 goal
|> Thm.prop_of
|> curry (op =) goal
|> (fn x => if not x then error "failed" else ())
end›

end
end

(*

Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
1         assume          8         8
2         hole            0         0
3         true            1         1
4         false           1         1
5         not_not         3         3
6,7       resolution      3         3
8         tautology       1         1
9         contraction     8         8
10        subproof        0         0
--------------------------------------------
                          25        25


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
11        la_generic      2         2
12        lia_generic     1         1
13        la_disequality  4         4
14        la_totality     2         2
15        la_tautology    9         9
16        la_mult_pos     3         3
17        la_mult_neg     0         0
18        bind            0         0
19        sko_ex          0         0
20        sko_forall      0         0
--------------------------------------------
                          21        21


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
21        forall_inst     0         0
22        refl            0         0
23        trans           5         5
24        cong            3         3
25        eq_reflexive    3         3
26        eq_transitive   4         4
27        eq_congruent    3         3
28        eq_congruent_pred 2       2
29        qnt_cnf         5         4
30        and             4         4
--------------------------------------------
                          29        28


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
31        not_or          6         6
32        or              3         3
33        weakening       5         5
34        reordering      4         4
35        shuffle         15        15
36        not_and         5         5
37        xor1            4         4
38        xor2            4         4
39        not_xor         4         4
40        not_xor2        4         4
--------------------------------------------
                          54        54


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
41        implies         5         5
42        not_implies1    5         5
43        not_implies2    5         5
44        equiv1          5         5
45        equiv2          5         5
46        not_equiv1      5         5
47        not_equiv2      5         5
48        and_pos         9         9
49        and_neg         9         9
50        or_pos          7         7
--------------------------------------------
                          60        60


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
51        or_neg          12        12
52        xor_pos1        7         7
53        xor_pos2        7         7
54        xor_neg1        5         5
55        xor_neg2        5         5
56        implies_pos     6         6
57        implies_neg1    6         6
58        implies_neg2    5         5
59        equiv_pos1      5         5
60        equiv_pos2      5         5
--------------------------------------------
                          63        63


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
61        equiv_neg1      5         5
62        equiv_neg2      5         5
63        ite1            3         3
64        ite2            3         3
65        ite_pos1        6         6
66        ite_pos2        6         6
67        ite_neg1        5         5
68        ite_neg2        5         5
69        not_ite1        3         3
70        not_ite2        3         3
--------------------------------------------
                          44        44


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
71        connective_def  10        10
72        and_simplify    4         4
73        or_simplify     4         4
74        not_simplify    6         6
75        implies_simplify 9        9
76        equiv_simplify  8         8
77        bool_simplify   7         7
78        ac_simp         4         4
79        ite_simplify    12        12
80        qnt_simplify    4         4
--------------------------------------------
                          68        68


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
81        onepoint        0         0
82        qnt_join        8         8
83        qnt_rm_ununsed  6         6
84        eq_simplify     4         4
85        div_simplify    9         9
86        prod_simplify   6         6
87        unary_minus_simplify  3   3
88        minus_simplify  4         4
89        sum_simplify    3         3
90        comp_simplify   9         9
--------------------------------------------
                          52        52


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
91        let             0         0
92        bind_let        0         0
93        distinct_elim   6         6
94        la_rw_eq1       3         3
95        nary_elim       2         2
96        bfun_elim       0         0
97        ite_intro       9         9
98        bitblast_extract 0        0
99        bitblast_ult    0         0
100       bitblast_add    0         0
--------------------------------------------
                          20        20


Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
101       sym             0         0
102       not_symm        0         0
103       eq_symmetric    0         0
104       miniscope_distribute  10  10
105       miniscope_split 14        14
106       miniscope_ite   2         2
107       aci_simp        0         0
--------------------------------------------
                          26        26




Rule Nr   Name            Nr Tests  Nr Success
--------------------------------------------
Total                     462       461

*)

end