theory Bug2
imports Main
begin
  datatype 'a M_nres = is_fail: FAIL | SPEC "'a \<Rightarrow> bool"

  definition "is_res m x \<equiv> case m of FAIL \<Rightarrow> True | SPEC P \<Rightarrow> P x"
  
  datatype ('a,'s) M_state = M_STATE (run: "'s \<Rightarrow> ('a\<times>'s) M_nres")
  
  lemma "\<lbrakk>\<forall>x y. (\<forall>xa s. is_fail (run (x xa) s) \<or>
                   is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
                   (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
           (\<forall>s. is_fail (run (B x) s) \<or>
                is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
                (\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
     \<And>y. \<forall>x ya. (\<forall>xa s. is_fail (run (x xa) s) \<or>
                         is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
                         (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
                 (\<forall>s. is_fail (run (C y x) s) \<or>
                      is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
                      (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a, b)))\<rbrakk>
    \<Longrightarrow> \<forall>x y. (\<forall>xa s.
                  is_fail (run (x xa) s) \<or>
                  is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
                  (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
              (\<forall>s. is_fail (run (B x) s) \<or>
                   (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
                   (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and> is_fail (run (C a y) b))) =
                   (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b))) \<and>
                   (\<forall>a b. (is_fail (run (B y) s) \<or>
                           (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y) ba) (a, b))) =
                          (is_fail (run (B x) s) \<or>
                           (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x) ba) (a, b)))))"  
    apply (smt (verit))
    (**
exception THM 0 raised (line 312 of "drule.ML"):
  OF: no unifiers
  ?x = (SOME x. \<not> ?P x) \<Longrightarrow> (\<forall>x. ?P x) = ?P ?x
  veriT_sk4__ =
  (SOME veriT_vr67.
      is_res (run (B veriT_sk1__) veriT_sk2__) (veriT_sk3__, veriT_vr67) \<and>
      is_fail (run (C veriT_sk3__ veriT_sk1__) veriT_vr67))
    [veriT_sk4__ =
     (SOME veriT_vr67.
         is_res (run (B veriT_sk1__) veriT_sk2__) (veriT_sk3__, veriT_vr67) \<and>
         is_fail (run (C veriT_sk3__ veriT_sk1__) veriT_vr67))]    
    *)
     oops
    
end