Z3---4.15.1.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SWV907-1 : TPTP v9.0.0. Released v4.1.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n015.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sat Jun 21 05:36:19 AM UTC 2025

% Result   : Unsatisfiable 0.73s 0.90s
% Output   : Proof 0.78s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   11
%            Number of leaves      :   39
% Syntax   : Number of formulae    :   89 (  28 unt;   0 typ;   0 def)
%            Number of atoms       :  440 (  14 equ)
%            Maximal formula atoms :   16 (   4 avg)
%            Number of connectives :  612 ( 286   ~; 277   |;   0   &)
%                                         (  49 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    9 (   5 avg)
%            Maximal term depth    :    5 (   2 avg)
%            Number of FOOLs       :   25 (  25 fml;   0 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   12 (  10 usr;   3 prp; 0-3 aty)
%            Number of functors    :   16 (  16 usr;   7 con; 0-5 aty)
%            Number of variables   :  143 ( 131   !;   0   ?; 143   :)

% Comments : 
%------------------------------------------------------------------------------
tff(c_lessequals_type,type,
    c_lessequals: ( $i * $i * $i ) > $o ).

tff(tc_fun_type,type,
    tc_fun: ( $i * $i ) > $i ).

tff(tc_bool_type,type,
    tc_bool: $i ).

tff(tc_Hoare__Mirabelle_Otriple_type,type,
    tc_Hoare__Mirabelle_Otriple: $i > $i ).

tff(tc_Com_Ostate_type,type,
    tc_Com_Ostate: $i ).

tff(c_Set_Oimage_type,type,
    c_Set_Oimage: ( $i * $i * $i * $i ) > $i ).

tff(tc_Com_Opname_type,type,
    tc_Com_Opname: $i ).

tff(c_Map_Odom_type,type,
    c_Map_Odom: ( $i * $i * $i ) > $i ).

tff(tc_Com_Ocom_type,type,
    tc_Com_Ocom: $i ).

tff(c_Com_Obody_type,type,
    c_Com_Obody: $i ).

tff(c_COMBB_type,type,
    c_COMBB: ( $i * $i * $i * $i * $i ) > $i ).

tff(tc_Option_Ooption_type,type,
    tc_Option_Ooption: $i > $i ).

tff(c_Option_Othe_type,type,
    c_Option_Othe: $i > $i ).

tff(c_Hoare__Mirabelle_OMGT_type,type,
    c_Hoare__Mirabelle_OMGT: $i ).

tff(c_Hoare__Mirabelle_Ohoare__derivs_type,type,
    c_Hoare__Mirabelle_Ohoare__derivs: ( $i * $i * $i ) > $o ).

tff(c_Com_Ocom_OBODY_type,type,
    c_Com_Ocom_OBODY: $i ).

tff(c_Lattices_Oupper__semilattice__class_Osup_type,type,
    c_Lattices_Oupper__semilattice__class_Osup: ( $i * $i * $i ) > $i ).

tff(c_Orderings_Obot__class_Obot_type,type,
    c_Orderings_Obot__class_Obot: $i > $i ).

tff(c_Finite__Set_Ofinite_type,type,
    c_Finite__Set_Ofinite: ( $i * $i ) > $o ).

tff(c_Com_OWT__bodies_type,type,
    c_Com_OWT__bodies: $o ).

tff(c_Hoare__Mirabelle_Ostate__not__singleton_type,type,
    c_Hoare__Mirabelle_Ostate__not__singleton: $o ).

tff(class_Orderings_Oorder_type,type,
    class_Orderings_Oorder: $i > $o ).

tff(1,plain,
    ^ [T_a: $i,V_B: $i] :
      refl(( ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B )
      <=> ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ) )),
    inference(bind,[status(th)],[]) ).

tff(2,plain,
    ( ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B )
  <=> ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ) ),
    inference(quant_intro,[status(thm)],[1]) ).

tff(3,plain,
    ( ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B )
  <=> ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(4,axiom,
    ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).

tff(5,plain,
    ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ),
    inference(modus_ponens,[status(thm)],[4,3]) ).

tff(6,plain,
    ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ),
    inference(skolemize,[status(sab)],[5]) ).

tff(7,plain,
    ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B ),
    inference(modus_ponens,[status(thm)],[6,2]) ).

tff(8,plain,
    ( ~ ! [T_a: $i,V_B: $i] : ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = V_B )
    | ( c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) = c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(9,plain,
    c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) = c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
    inference(unit_resolution,[status(thm)],[8,7]) ).

tff(10,plain,
    c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) = c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
    inference(symmetry,[status(thm)],[9]) ).

tff(11,plain,
    ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
  <=> c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(monotonicity,[status(thm)],[10]) ).

tff(12,plain,
    ( c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
  <=> c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(symmetry,[status(thm)],[11]) ).

tff(13,plain,
    ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
  <=> ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(monotonicity,[status(thm)],[12]) ).

tff(14,plain,
    ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
  <=> ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(rewrite,[status(thm)],[]) ).

tff(15,axiom,
    ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).

tff(16,plain,
    ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
    inference(modus_ponens,[status(thm)],[15,14]) ).

tff(17,plain,
    ( c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
  <=> c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) ),
    inference(rewrite,[status(thm)],[]) ).

tff(18,axiom,
    c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__dom__body_0) ).

tff(19,plain,
    c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
    inference(modus_ponens,[status(thm)],[18,17]) ).

tff(20,plain,
    ^ [V_G: $i,V_Procs: $i] :
      refl(( ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      <=> ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) )),
    inference(bind,[status(th)],[]) ).

tff(21,plain,
    ( ! [V_G: $i,V_Procs: $i] :
        ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ! [V_G: $i,V_Procs: $i] :
        ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(quant_intro,[status(thm)],[20]) ).

tff(22,plain,
    ( ! [V_G: $i,V_Procs: $i] :
        ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ! [V_G: $i,V_Procs: $i] :
        ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(23,plain,
    ^ [V_G: $i,V_Procs: $i] :
      trans(monotonicity(rewrite(( ( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
              | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname) )
          <=> ( ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
              | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) )),
          ( ( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
        <=> ( ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) )),
        rewrite(( ( ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
        <=> ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) )),
        ( ( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      <=> ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) )),
    inference(bind,[status(th)],[]) ).

tff(24,plain,
    ( ! [V_G: $i,V_Procs: $i] :
        ( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ! [V_G: $i,V_Procs: $i] :
        ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
        | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
        | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(quant_intro,[status(thm)],[23]) ).

tff(25,axiom,
    ! [V_G: $i,V_Procs: $i] :
      ( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_MGT__Body_0) ).

tff(26,plain,
    ! [V_G: $i,V_Procs: $i] :
      ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(modus_ponens,[status(thm)],[25,24]) ).

tff(27,plain,
    ! [V_G: $i,V_Procs: $i] :
      ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(modus_ponens,[status(thm)],[26,22]) ).

tff(28,plain,
    ! [V_G: $i,V_Procs: $i] :
      ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(skolemize,[status(sab)],[27]) ).

tff(29,plain,
    ! [V_G: $i,V_Procs: $i] :
      ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(modus_ponens,[status(thm)],[28,21]) ).

tff(30,plain,
    ( ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(31,plain,
    ( ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ( c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(32,plain,
    ( ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(monotonicity,[status(thm)],[31]) ).

tff(33,plain,
    ( ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ( ~ ! [V_G: $i,V_Procs: $i] :
            ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
            | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
            | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
      | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(transitivity,[status(thm)],[32,30]) ).

tff(34,plain,
    ( ~ ! [V_G: $i,V_Procs: $i] :
          ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
    | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
    | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
    | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(35,plain,
    ( ~ ! [V_G: $i,V_Procs: $i] :
          ( ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
          | ~ c_Finite__Set_Ofinite(V_Procs,tc_Com_Opname)
          | c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),V_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
    | c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
    | ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)
    | ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(modus_ponens,[status(thm)],[34,33]) ).

tff(36,plain,
    ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
    inference(unit_resolution,[status(thm)],[35,29,19,16]) ).

tff(37,plain,
    ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
    inference(modus_ponens,[status(thm)],[36,13]) ).

tff(38,plain,
    ( c_Com_OWT__bodies
  <=> c_Com_OWT__bodies ),
    inference(rewrite,[status(thm)],[]) ).

tff(39,axiom,
    c_Com_OWT__bodies,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).

tff(40,plain,
    c_Com_OWT__bodies,
    inference(modus_ponens,[status(thm)],[39,38]) ).

tff(41,plain,
    ( c_Hoare__Mirabelle_Ostate__not__singleton
  <=> c_Hoare__Mirabelle_Ostate__not__singleton ),
    inference(rewrite,[status(thm)],[]) ).

tff(42,axiom,
    c_Hoare__Mirabelle_Ostate__not__singleton,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).

tff(43,plain,
    c_Hoare__Mirabelle_Ostate__not__singleton,
    inference(modus_ponens,[status(thm)],[42,41]) ).

tff(44,plain,
    ^ [V_F: $i] :
      refl(( ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_Com_OWT__bodies )
      <=> ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_Com_OWT__bodies ) )),
    inference(bind,[status(th)],[]) ).

tff(45,plain,
    ( ! [V_F: $i] :
        ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_Com_OWT__bodies )
  <=> ! [V_F: $i] :
        ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_Com_OWT__bodies ) ),
    inference(quant_intro,[status(thm)],[44]) ).

tff(46,plain,
    ( ! [V_F: $i] :
        ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_Com_OWT__bodies )
  <=> ! [V_F: $i] :
        ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_Com_OWT__bodies ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(47,plain,
    ^ [V_F: $i] :
      trans(monotonicity(trans(monotonicity(rewrite(( ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
                  | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) )
              <=> ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
                  | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate) ) )),
              ( ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
                | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
                | ~ c_Com_OWT__bodies )
            <=> ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
                | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
                | ~ c_Com_OWT__bodies ) )),
            rewrite(( ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
                | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
                | ~ c_Com_OWT__bodies )
            <=> ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
                | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
                | ~ c_Com_OWT__bodies ) )),
            ( ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
              | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
              | ~ c_Com_OWT__bodies )
          <=> ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
              | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
              | ~ c_Com_OWT__bodies ) )),
          ( ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | ~ c_Com_OWT__bodies
            | ~ c_Hoare__Mirabelle_Ostate__not__singleton )
        <=> ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies
            | ~ c_Hoare__Mirabelle_Ostate__not__singleton ) )),
        rewrite(( ( ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies
            | ~ c_Hoare__Mirabelle_Ostate__not__singleton )
        <=> ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies ) )),
        ( ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | ~ c_Com_OWT__bodies
          | ~ c_Hoare__Mirabelle_Ostate__not__singleton )
      <=> ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_Com_OWT__bodies ) )),
    inference(bind,[status(th)],[]) ).

tff(48,plain,
    ( ! [V_F: $i] :
        ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | ~ c_Com_OWT__bodies
        | ~ c_Hoare__Mirabelle_Ostate__not__singleton )
  <=> ! [V_F: $i] :
        ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
        | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
        | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
        | ~ c_Com_OWT__bodies ) ),
    inference(quant_intro,[status(thm)],[47]) ).

tff(49,axiom,
    ! [V_F: $i] :
      ( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
      | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | ~ c_Com_OWT__bodies
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_MGF__lemma2__simult_0) ).

tff(50,plain,
    ! [V_F: $i] :
      ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
      | ~ c_Com_OWT__bodies ),
    inference(modus_ponens,[status(thm)],[49,48]) ).

tff(51,plain,
    ! [V_F: $i] :
      ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
      | ~ c_Com_OWT__bodies ),
    inference(modus_ponens,[status(thm)],[50,46]) ).

tff(52,plain,
    ! [V_F: $i] :
      ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
      | ~ c_Com_OWT__bodies ),
    inference(skolemize,[status(sab)],[51]) ).

tff(53,plain,
    ! [V_F: $i] :
      ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
      | ~ c_Com_OWT__bodies ),
    inference(modus_ponens,[status(thm)],[52,45]) ).

tff(54,plain,
    ( ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_Com_OWT__bodies
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) )
  <=> ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_Com_OWT__bodies
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(55,plain,
    ( ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Com_OWT__bodies )
  <=> ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_Com_OWT__bodies
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(56,plain,
    ( ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Com_OWT__bodies )
  <=> ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_Com_OWT__bodies
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(monotonicity,[status(thm)],[55]) ).

tff(57,plain,
    ( ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
      | ~ c_Com_OWT__bodies )
  <=> ( ~ ! [V_F: $i] :
            ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
            | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
            | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
            | ~ c_Com_OWT__bodies )
      | ~ c_Hoare__Mirabelle_Ostate__not__singleton
      | ~ c_Com_OWT__bodies
      | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
    inference(transitivity,[status(thm)],[56,54]) ).

tff(58,plain,
    ( ~ ! [V_F: $i] :
          ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_Com_OWT__bodies )
    | ~ c_Hoare__Mirabelle_Ostate__not__singleton
    | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
    | ~ c_Com_OWT__bodies ),
    inference(quant_inst,[status(thm)],[]) ).

tff(59,plain,
    ( ~ ! [V_F: $i] :
          ( ~ c_Hoare__Mirabelle_Ostate__not__singleton
          | ~ c_lessequals(V_F,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
          | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),V_F,tc_Com_Ostate)
          | ~ c_Com_OWT__bodies )
    | ~ c_Hoare__Mirabelle_Ostate__not__singleton
    | ~ c_Com_OWT__bodies
    | ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(modus_ponens,[status(thm)],[58,57]) ).

tff(60,plain,
    ( ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
    inference(unit_resolution,[status(thm)],[59,53,43,40]) ).

tff(61,plain,
    ~ c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
    inference(unit_resolution,[status(thm)],[60,37]) ).

tff(62,plain,
    ( class_Orderings_Oorder(tc_bool)
  <=> class_Orderings_Oorder(tc_bool) ),
    inference(rewrite,[status(thm)],[]) ).

tff(63,axiom,
    class_Orderings_Oorder(tc_bool),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Orderings_Oorder) ).

tff(64,plain,
    class_Orderings_Oorder(tc_bool),
    inference(modus_ponens,[status(thm)],[63,62]) ).

tff(65,plain,
    ^ [T_1: $i,T_2: $i] :
      refl(( ( class_Orderings_Oorder(tc_fun(T_2,T_1))
          | ~ class_Orderings_Oorder(T_1) )
      <=> ( class_Orderings_Oorder(tc_fun(T_2,T_1))
          | ~ class_Orderings_Oorder(T_1) ) )),
    inference(bind,[status(th)],[]) ).

tff(66,plain,
    ( ! [T_1: $i,T_2: $i] :
        ( class_Orderings_Oorder(tc_fun(T_2,T_1))
        | ~ class_Orderings_Oorder(T_1) )
  <=> ! [T_1: $i,T_2: $i] :
        ( class_Orderings_Oorder(tc_fun(T_2,T_1))
        | ~ class_Orderings_Oorder(T_1) ) ),
    inference(quant_intro,[status(thm)],[65]) ).

tff(67,plain,
    ( ! [T_1: $i,T_2: $i] :
        ( class_Orderings_Oorder(tc_fun(T_2,T_1))
        | ~ class_Orderings_Oorder(T_1) )
  <=> ! [T_1: $i,T_2: $i] :
        ( class_Orderings_Oorder(tc_fun(T_2,T_1))
        | ~ class_Orderings_Oorder(T_1) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(68,axiom,
    ! [T_1: $i,T_2: $i] :
      ( class_Orderings_Oorder(tc_fun(T_2,T_1))
      | ~ class_Orderings_Oorder(T_1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_fun__Orderings_Oorder) ).

tff(69,plain,
    ! [T_1: $i,T_2: $i] :
      ( class_Orderings_Oorder(tc_fun(T_2,T_1))
      | ~ class_Orderings_Oorder(T_1) ),
    inference(modus_ponens,[status(thm)],[68,67]) ).

tff(70,plain,
    ! [T_1: $i,T_2: $i] :
      ( class_Orderings_Oorder(tc_fun(T_2,T_1))
      | ~ class_Orderings_Oorder(T_1) ),
    inference(skolemize,[status(sab)],[69]) ).

tff(71,plain,
    ! [T_1: $i,T_2: $i] :
      ( class_Orderings_Oorder(tc_fun(T_2,T_1))
      | ~ class_Orderings_Oorder(T_1) ),
    inference(modus_ponens,[status(thm)],[70,66]) ).

tff(72,plain,
    ( ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | ~ class_Orderings_Oorder(tc_bool)
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) )
  <=> ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | ~ class_Orderings_Oorder(tc_bool)
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(73,plain,
    ( ( class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | ~ class_Orderings_Oorder(tc_bool) )
  <=> ( ~ class_Orderings_Oorder(tc_bool)
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(74,plain,
    ( ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | ~ class_Orderings_Oorder(tc_bool) )
  <=> ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | ~ class_Orderings_Oorder(tc_bool)
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ) ),
    inference(monotonicity,[status(thm)],[73]) ).

tff(75,plain,
    ( ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | ~ class_Orderings_Oorder(tc_bool) )
  <=> ( ~ ! [T_1: $i,T_2: $i] :
            ( class_Orderings_Oorder(tc_fun(T_2,T_1))
            | ~ class_Orderings_Oorder(T_1) )
      | ~ class_Orderings_Oorder(tc_bool)
      | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ) ),
    inference(transitivity,[status(thm)],[74,72]) ).

tff(76,plain,
    ( ~ ! [T_1: $i,T_2: $i] :
          ( class_Orderings_Oorder(tc_fun(T_2,T_1))
          | ~ class_Orderings_Oorder(T_1) )
    | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | ~ class_Orderings_Oorder(tc_bool) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(77,plain,
    ( ~ ! [T_1: $i,T_2: $i] :
          ( class_Orderings_Oorder(tc_fun(T_2,T_1))
          | ~ class_Orderings_Oorder(T_1) )
    | ~ class_Orderings_Oorder(tc_bool)
    | class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ),
    inference(modus_ponens,[status(thm)],[76,75]) ).

tff(78,plain,
    class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),
    inference(unit_resolution,[status(thm)],[77,71,64]) ).

tff(79,plain,
    ^ [V_x: $i,T_a: $i] :
      refl(( ( ~ class_Orderings_Oorder(T_a)
          | c_lessequals(V_x,V_x,T_a) )
      <=> ( ~ class_Orderings_Oorder(T_a)
          | c_lessequals(V_x,V_x,T_a) ) )),
    inference(bind,[status(th)],[]) ).

tff(80,plain,
    ( ! [V_x: $i,T_a: $i] :
        ( ~ class_Orderings_Oorder(T_a)
        | c_lessequals(V_x,V_x,T_a) )
  <=> ! [V_x: $i,T_a: $i] :
        ( ~ class_Orderings_Oorder(T_a)
        | c_lessequals(V_x,V_x,T_a) ) ),
    inference(quant_intro,[status(thm)],[79]) ).

tff(81,plain,
    ( ! [V_x: $i,T_a: $i] :
        ( ~ class_Orderings_Oorder(T_a)
        | c_lessequals(V_x,V_x,T_a) )
  <=> ! [V_x: $i,T_a: $i] :
        ( ~ class_Orderings_Oorder(T_a)
        | c_lessequals(V_x,V_x,T_a) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(82,axiom,
    ! [V_x: $i,T_a: $i] :
      ( ~ class_Orderings_Oorder(T_a)
      | c_lessequals(V_x,V_x,T_a) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__eq__iff_0) ).

tff(83,plain,
    ! [V_x: $i,T_a: $i] :
      ( ~ class_Orderings_Oorder(T_a)
      | c_lessequals(V_x,V_x,T_a) ),
    inference(modus_ponens,[status(thm)],[82,81]) ).

tff(84,plain,
    ! [V_x: $i,T_a: $i] :
      ( ~ class_Orderings_Oorder(T_a)
      | c_lessequals(V_x,V_x,T_a) ),
    inference(skolemize,[status(sab)],[83]) ).

tff(85,plain,
    ! [V_x: $i,T_a: $i] :
      ( ~ class_Orderings_Oorder(T_a)
      | c_lessequals(V_x,V_x,T_a) ),
    inference(modus_ponens,[status(thm)],[84,80]) ).

tff(86,plain,
    ( ( ~ ! [V_x: $i,T_a: $i] :
            ( ~ class_Orderings_Oorder(T_a)
            | c_lessequals(V_x,V_x,T_a) )
      | ~ class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) )
  <=> ( ~ ! [V_x: $i,T_a: $i] :
            ( ~ class_Orderings_Oorder(T_a)
            | c_lessequals(V_x,V_x,T_a) )
      | ~ class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
      | c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(87,plain,
    ( ~ ! [V_x: $i,T_a: $i] :
          ( ~ class_Orderings_Oorder(T_a)
          | c_lessequals(V_x,V_x,T_a) )
    | ~ class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(88,plain,
    ( ~ ! [V_x: $i,T_a: $i] :
          ( ~ class_Orderings_Oorder(T_a)
          | c_lessequals(V_x,V_x,T_a) )
    | ~ class_Orderings_Oorder(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
    | c_lessequals(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ),
    inference(modus_ponens,[status(thm)],[87,86]) ).

tff(89,plain,
    $false,
    inference(unit_resolution,[status(thm)],[88,85,78,61]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem    : SWV907-1 : TPTP v9.0.0. Released v4.1.0.
% 0.07/0.13  % Command    : run_E %s %d THM
% 0.13/0.34  % Computer : n015.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit   : 300
% 0.13/0.34  % WCLimit    : 300
% 0.13/0.34  % DateTime   : Fri Jun 20 11:01:55 EDT 2025
% 0.13/0.34  % CPUTime    : 
% 0.73/0.90  % SZS status Unsatisfiable
% 0.73/0.90  % SZS output start Proof
% See solution above
% 0.78/0.95  % E exiting
%------------------------------------------------------------------------------