TPTP Problem File: SWW474^1.p

View Solutions - Solve Problem

%------------------------------------------------------------------------------
% File     : SWW474^1 : TPTP v7.1.0. Released v5.3.0.
% Domain   : Software Verification
% Problem  : Hoare's Logic with Procedures line 440, 100 axioms selected
% Version  : Especial.
% English  :

% Refs     : [BN10]  Boehme & Nipkow (2010), Sledgehammer: Judgement Day
%          : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% Source   : [Bla11]
% Names    : hoare_100_thf_l440 [Bla11]

% Status   : Theorem
% Rating   : 0.38 v7.1.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.40 v6.2.0, 0.43 v6.1.0, 0.57 v5.5.0, 0.50 v5.4.0, 0.80 v5.3.0
% Syntax   : Number of formulae    :  396 (   2 unit;  80 type;   0 defn)
%            Number of atoms       : 2888 ( 265 equality;1506 variable)
%            Maximal formula depth :   17 (   7 average)
%            Number of connectives : 2132 (  90   ~;  24   |;  36   &;1615   @)
%                                         (  53 <=>; 314  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of type conns  : 1124 (1124   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   87 (  80   :;   0   =)
%            Number of variables   :  776 (  38 sgn; 680   !;   7   ?;  89   ^)
%                                         ( 776   :;   0  !>;   0  ?*)
%                                         (   0  @-;   0  @+)
% SPC      : TH0_THM_EQU_NAR

% Comments : This file was generated by Isabelle (most likely Sledgehammer)
%            2011-08-09 19:26:26
%------------------------------------------------------------------------------
%----Should-be-implicit typings (4)
thf(ty_ty_tc__Com__Ocom,type,(
    com: $tType )).

thf(ty_ty_tc__Com__Opname,type,(
    pname: $tType )).

thf(ty_ty_tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostate_J,type,(
    hoare_1262092251_state: $tType )).

thf(ty_ty_tc__Option__Ooption_Itc__Com__Ocom_J,type,(
    option_com: $tType )).

%----Explicit typings (76)
thf(sy_c_Com_OWT,type,(
    wt: com > $o )).

thf(sy_c_Com_OWT__bodies,type,(
    wT_bodies: $o )).

thf(sy_c_Com_Obody,type,(
    body: pname > option_com )).

thf(sy_c_Com_Ocom_OBODY,type,(
    body_1: pname > com )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_M_Eo,type,(
    finite1648353812_o_o_o: ( ( ( ( pname > $o ) > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbq,type,(
    finite734360985_o_o_o: ( ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    finite1066544169me_o_o: ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Ot,type,(
    finite1303896758te_o_o: ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_Itc__Com__Opname_M_Eo_J,type,(
    finite297249702name_o: ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_,type,(
    finite1423311111tate_o: ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000tc__Com__Opname,type,(
    finite_finite_pname: ( pname > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__C,type,(
    finite1178804552_state: ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_OMGT,type,(
    hoare_Mirabelle_MGT: com > hoare_1262092251_state )).

thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ohoare__derivs_000tc__Com__Ostate,type,(
    hoare_930741239_state: ( hoare_1262092251_state > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ostate__not__singleton,type,(
    hoare_1821564147gleton: $o )).

thf(sy_c_Map_Odom_000_062_Itc__Com__Opname_M_Eo_J_000tc__Com__Ocom,type,(
    dom_pname_o_com: ( ( pname > $o ) > option_com ) > ( pname > $o ) > $o )).

thf(sy_c_Map_Odom_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__O,type,(
    dom_Ho1489634536_o_com: ( ( hoare_1262092251_state > $o ) > option_com ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Map_Odom_000tc__Com__Opname_000tc__Com__Ocom,type,(
    dom_pname_com: ( pname > option_com ) > pname > $o )).

thf(sy_c_Option_Ooption_OSome_000tc__Com__Ocom,type,(
    some_com: com > option_com )).

thf(sy_c_Option_Othe_000tc__Com__Ocom,type,(
    the_com: option_com > com )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo,type,(
    bot_bot_pname_o_o_o: ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_I_062_I_062_Itc__Hoare____Mirabelle____g,type,(
    bot_bo388435036_o_o_o: ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    bot_bot_pname_o_o: ( pname > $o ) > $o )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsb,type,(
    bot_bo1962689075te_o_o: ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_Itc__Com__Opname_M_Eo_J,type,(
    bot_bot_pname_o: pname > $o )).

thf(sy_c_Orderings_Obot__class_Obot_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__O,type,(
    bot_bo113204042tate_o: hoare_1262092251_state > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J,type,(
    ord_le1828183645_o_o_o: ( ( ( pname > $o ) > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_I_062_Itc__Hoare____Mirabelle,type,(
    ord_le1891858320_o_o_o: ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_,type,(
    ord_le1205211808me_o_o: ( ( pname > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_Itc__Hoare____Mirabelle____gh,type,(
    ord_le2012720639te_o_o: ( ( hoare_1262092251_state > $o ) > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_Itc__Com__Opname_M_Eo_J,type,(
    ord_less_eq_pname_o: ( pname > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_Itc__Hoare____Mirabelle____ghhkfsbq,type,(
    ord_le870406270tate_o: ( hoare_1262092251_state > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    collect_pname_o_o_o: ( ( ( ( pname > $o ) > $o ) > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otr,type,(
    collec101077467_o_o_o: ( ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > $o ) > ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    collect_pname_o_o: ( ( ( pname > $o ) > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_I,type,(
    collec341954548te_o_o: ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_Itc__Com__Opname_M_Eo_J,type,(
    collect_pname_o: ( ( pname > $o ) > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Co,type,(
    collec313158217tate_o: ( ( hoare_1262092251_state > $o ) > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Set_OCollect_000tc__Com__Opname,type,(
    collect_pname: ( pname > $o ) > pname > $o )).

thf(sy_c_Set_OCollect_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ost,type,(
    collec1121927558_state: ( hoare_1262092251_state > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_000tc__Com__Opname,type,(
    image_471733107_pname: ( ( ( pname > $o ) > $o ) > pname ) > ( ( ( pname > $o ) > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_000tc__Hoare____Mir,type,(
    image_1036078444_state: ( ( ( pname > $o ) > $o ) > hoare_1262092251_state ) > ( ( ( pname > $o ) > $o ) > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc,type,(
    image_893364936_pname: ( ( ( hoare_1262092251_state > $o ) > $o ) > pname ) > ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc_001,type,(
    image_165349207_state: ( ( ( hoare_1262092251_state > $o ) > $o ) > hoare_1262092251_state ) > ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Com__Opname_M_Eo_J_000tc__Com__Opname,type,(
    image_pname_o_pname: ( ( pname > $o ) > pname ) > ( ( pname > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Com__Opname_M_Eo_J_000tc__Hoare____Mirabelle____ghh,type,(
    image_1476171975_state: ( ( pname > $o ) > hoare_1262092251_state ) > ( ( pname > $o ) > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com_,type,(
    image_1820530197_pname: ( ( hoare_1262092251_state > $o ) > pname ) > ( ( hoare_1262092251_state > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__002,type,(
    image_234589002_state: ( ( hoare_1262092251_state > $o ) > hoare_1262092251_state ) > ( ( hoare_1262092251_state > $o ) > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    image_504089495me_o_o: ( pname > ( pname > $o ) > $o ) > ( pname > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_I_062_Itc__Hoare____Mirabelle____ghhk,type,(
    image_827868872te_o_o: ( pname > ( hoare_1262092251_state > $o ) > $o ) > ( pname > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_Itc__Com__Opname_M_Eo_J,type,(
    image_pname_pname_o: ( pname > pname > $o ) > ( pname > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq,type,(
    image_518521461tate_o: ( pname > hoare_1262092251_state > $o ) > ( pname > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000tc__Com__Opname,type,(
    image_pname_pname: ( pname > pname ) > ( pname > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otri,type,(
    image_669833818_state: ( pname > hoare_1262092251_state ) > ( pname > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_Set_Oimage_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostat,type,(
    image_333245000me_o_o: ( hoare_1262092251_state > ( pname > $o ) > $o ) > ( hoare_1262092251_state > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostat_003,type,(
    image_1731108951te_o_o: ( hoare_1262092251_state > ( hoare_1262092251_state > $o ) > $o ) > ( hoare_1262092251_state > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostat_004,type,(
    image_1320925383name_o: ( hoare_1262092251_state > pname > $o ) > ( hoare_1262092251_state > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostat_005,type,(
    image_1403668518tate_o: ( hoare_1262092251_state > hoare_1262092251_state > $o ) > ( hoare_1262092251_state > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostat_006,type,(
    image_202231862_pname: ( hoare_1262092251_state > pname ) > ( hoare_1262092251_state > $o ) > pname > $o )).

thf(sy_c_Set_Oinsert_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    insert_pname_o_o: ( ( pname > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_I_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It,type,(
    insert1691644879te_o_o: ( ( hoare_1262092251_state > $o ) > $o ) > ( ( ( hoare_1262092251_state > $o ) > $o ) > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_Itc__Com__Opname_M_Eo_J,type,(
    insert_pname_o: ( pname > $o ) > ( ( pname > $o ) > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com,type,(
    insert1042460334tate_o: ( hoare_1262092251_state > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_Set_Oinsert_000tc__Com__Opname,type,(
    insert_pname: pname > ( pname > $o ) > pname > $o )).

thf(sy_c_Set_Oinsert_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Osta,type,(
    insert81609953_state: hoare_1262092251_state > ( hoare_1262092251_state > $o ) > hoare_1262092251_state > $o )).

thf(sy_c_fequal_000_062_Itc__Com__Opname_M_Eo_J,type,(
    fequal_pname_o: ( pname > $o ) > ( pname > $o ) > $o )).

thf(sy_c_fequal_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ost,type,(
    fequal1529404211tate_o: ( hoare_1262092251_state > $o ) > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_c_fequal_000tc__Com__Opname,type,(
    fequal_pname: pname > pname > $o )).

thf(sy_c_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostate_J,type,(
    fequal1925511196_state: hoare_1262092251_state > hoare_1262092251_state > $o )).

thf(sy_c_member_000_062_Itc__Com__Opname_M_Eo_J,type,(
    member_pname_o: ( pname > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_member_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ost,type,(
    member907417095tate_o: ( hoare_1262092251_state > $o ) > ( ( hoare_1262092251_state > $o ) > $o ) > $o )).

thf(sy_c_member_000tc__Com__Opname,type,(
    member_pname: pname > ( pname > $o ) > $o )).

thf(sy_c_member_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com__Ostate_J,type,(
    member5164104_state: hoare_1262092251_state > ( hoare_1262092251_state > $o ) > $o )).

thf(sy_v_Fa,type,(
    fa: hoare_1262092251_state > $o )).

thf(sy_v_pn,type,(
    pn: pname )).

thf(sy_v_y,type,(
    y: com )).

%----Relevant facts (300)
thf(fact_0_empty,axiom,(
    ! [G: hoare_1262092251_state > $o] :
      ( hoare_930741239_state @ G @ bot_bo113204042tate_o ) )).

thf(fact_1_asm,axiom,(
    ! [Ts_6: hoare_1262092251_state > $o,G_8: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ Ts_6 @ G_8 )
     => ( hoare_930741239_state @ G_8 @ Ts_6 ) ) )).

thf(fact_2_weaken,axiom,(
    ! [Ts_5: hoare_1262092251_state > $o,G_7: hoare_1262092251_state > $o,Ts_4: hoare_1262092251_state > $o] :
      ( ( hoare_930741239_state @ G_7 @ Ts_4 )
     => ( ( ord_le870406270tate_o @ Ts_5 @ Ts_4 )
       => ( hoare_930741239_state @ G_7 @ Ts_5 ) ) ) )).

thf(fact_3_thin,axiom,(
    ! [G_6: hoare_1262092251_state > $o,G_5: hoare_1262092251_state > $o,Ts_3: hoare_1262092251_state > $o] :
      ( ( hoare_930741239_state @ G_5 @ Ts_3 )
     => ( ( ord_le870406270tate_o @ G_5 @ G_6 )
       => ( hoare_930741239_state @ G_6 @ Ts_3 ) ) ) )).

thf(fact_4_cut,axiom,(
    ! [G_4: hoare_1262092251_state > $o,G_3: hoare_1262092251_state > $o,Ts_2: hoare_1262092251_state > $o] :
      ( ( hoare_930741239_state @ G_3 @ Ts_2 )
     => ( ( hoare_930741239_state @ G_4 @ G_3 )
       => ( hoare_930741239_state @ G_4 @ Ts_2 ) ) ) )).

thf(fact_5_hoare__derivs_Oinsert,axiom,(
    ! [Ts_1: hoare_1262092251_state > $o,G_2: hoare_1262092251_state > $o,T_1: hoare_1262092251_state] :
      ( ( hoare_930741239_state @ G_2 @ ( insert81609953_state @ T_1 @ bot_bo113204042tate_o ) )
     => ( ( hoare_930741239_state @ G_2 @ Ts_1 )
       => ( hoare_930741239_state @ G_2 @ ( insert81609953_state @ T_1 @ Ts_1 ) ) ) ) )).

thf(fact_6_derivs__insertD,axiom,(
    ! [G_1: hoare_1262092251_state > $o,T: hoare_1262092251_state,Ts: hoare_1262092251_state > $o] :
      ( ( hoare_930741239_state @ G_1 @ ( insert81609953_state @ T @ Ts ) )
     => ( ( hoare_930741239_state @ G_1 @ ( insert81609953_state @ T @ bot_bo113204042tate_o ) )
        & ( hoare_930741239_state @ G_1 @ Ts ) ) ) )).

thf(fact_7_MGT__BodyN,axiom,(
    ! [Pn_1: pname,G: hoare_1262092251_state > $o] :
      ( ( hoare_930741239_state @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ ( body_1 @ Pn_1 ) ) @ G ) @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ ( the_com @ ( body @ Pn_1 ) ) ) @ bot_bo113204042tate_o ) )
     => ( hoare_930741239_state @ G @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ ( body_1 @ Pn_1 ) ) @ bot_bo113204042tate_o ) ) ) )).

thf(fact_8_finite__Collect__subsets,axiom,(
    ! [A_77: pname > $o] :
      ( ( finite_finite_pname @ A_77 )
     => ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [B_41: pname > $o] :
              ( ord_less_eq_pname_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_9_finite__Collect__subsets,axiom,(
    ! [A_77: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_77 )
     => ( finite1423311111tate_o
        @ ( collec313158217tate_o
          @ ^ [B_41: hoare_1262092251_state > $o] :
              ( ord_le870406270tate_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_10_finite__Collect__subsets,axiom,(
    ! [A_77: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_77 )
     => ( finite1648353812_o_o_o
        @ ( collect_pname_o_o_o
          @ ^ [B_41: ( ( pname > $o ) > $o ) > $o] :
              ( ord_le1828183645_o_o_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_11_finite__Collect__subsets,axiom,(
    ! [A_77: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ A_77 )
     => ( finite734360985_o_o_o
        @ ( collec101077467_o_o_o
          @ ^ [B_41: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
              ( ord_le1891858320_o_o_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_12_finite__Collect__subsets,axiom,(
    ! [A_77: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ A_77 )
     => ( finite1303896758te_o_o
        @ ( collec341954548te_o_o
          @ ^ [B_41: ( hoare_1262092251_state > $o ) > $o] :
              ( ord_le2012720639te_o_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_13_finite__Collect__subsets,axiom,(
    ! [A_77: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_77 )
     => ( finite1066544169me_o_o
        @ ( collect_pname_o_o
          @ ^ [B_41: ( pname > $o ) > $o] :
              ( ord_le1205211808me_o_o @ B_41 @ A_77 ) ) ) ) )).

thf(fact_14_finite__imageI,axiom,(
    ! [H: pname > hoare_1262092251_state,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite1178804552_state @ ( image_669833818_state @ H @ F_17 ) ) ) )).

thf(fact_15_finite__imageI,axiom,(
    ! [H: ( ( pname > $o ) > $o ) > pname,F_17: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ F_17 )
     => ( finite_finite_pname @ ( image_471733107_pname @ H @ F_17 ) ) ) )).

thf(fact_16_finite__imageI,axiom,(
    ! [H: ( ( hoare_1262092251_state > $o ) > $o ) > pname,F_17: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ F_17 )
     => ( finite_finite_pname @ ( image_893364936_pname @ H @ F_17 ) ) ) )).

thf(fact_17_finite__imageI,axiom,(
    ! [H: ( hoare_1262092251_state > $o ) > pname,F_17: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ F_17 )
     => ( finite_finite_pname @ ( image_1820530197_pname @ H @ F_17 ) ) ) )).

thf(fact_18_finite__imageI,axiom,(
    ! [H: ( pname > $o ) > pname,F_17: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_17 )
     => ( finite_finite_pname @ ( image_pname_o_pname @ H @ F_17 ) ) ) )).

thf(fact_19_finite__imageI,axiom,(
    ! [H: ( ( pname > $o ) > $o ) > hoare_1262092251_state,F_17: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ F_17 )
     => ( finite1178804552_state @ ( image_1036078444_state @ H @ F_17 ) ) ) )).

thf(fact_20_finite__imageI,axiom,(
    ! [H: ( ( hoare_1262092251_state > $o ) > $o ) > hoare_1262092251_state,F_17: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ F_17 )
     => ( finite1178804552_state @ ( image_165349207_state @ H @ F_17 ) ) ) )).

thf(fact_21_finite__imageI,axiom,(
    ! [H: ( hoare_1262092251_state > $o ) > hoare_1262092251_state,F_17: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ F_17 )
     => ( finite1178804552_state @ ( image_234589002_state @ H @ F_17 ) ) ) )).

thf(fact_22_finite__imageI,axiom,(
    ! [H: ( pname > $o ) > hoare_1262092251_state,F_17: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_17 )
     => ( finite1178804552_state @ ( image_1476171975_state @ H @ F_17 ) ) ) )).

thf(fact_23_finite__imageI,axiom,(
    ! [H: pname > ( pname > $o ) > $o,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite1066544169me_o_o @ ( image_504089495me_o_o @ H @ F_17 ) ) ) )).

thf(fact_24_finite__imageI,axiom,(
    ! [H: pname > ( hoare_1262092251_state > $o ) > $o,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite1303896758te_o_o @ ( image_827868872te_o_o @ H @ F_17 ) ) ) )).

thf(fact_25_finite__imageI,axiom,(
    ! [H: pname > hoare_1262092251_state > $o,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite1423311111tate_o @ ( image_518521461tate_o @ H @ F_17 ) ) ) )).

thf(fact_26_finite__imageI,axiom,(
    ! [H: pname > pname > $o,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite297249702name_o @ ( image_pname_pname_o @ H @ F_17 ) ) ) )).

thf(fact_27_finite__imageI,axiom,(
    ! [H: hoare_1262092251_state > ( pname > $o ) > $o,F_17: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_17 )
     => ( finite1066544169me_o_o @ ( image_333245000me_o_o @ H @ F_17 ) ) ) )).

thf(fact_28_finite__imageI,axiom,(
    ! [H: hoare_1262092251_state > ( hoare_1262092251_state > $o ) > $o,F_17: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_17 )
     => ( finite1303896758te_o_o @ ( image_1731108951te_o_o @ H @ F_17 ) ) ) )).

thf(fact_29_finite__imageI,axiom,(
    ! [H: hoare_1262092251_state > hoare_1262092251_state > $o,F_17: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_17 )
     => ( finite1423311111tate_o @ ( image_1403668518tate_o @ H @ F_17 ) ) ) )).

thf(fact_30_finite__imageI,axiom,(
    ! [H: hoare_1262092251_state > pname > $o,F_17: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_17 )
     => ( finite297249702name_o @ ( image_1320925383name_o @ H @ F_17 ) ) ) )).

thf(fact_31_finite__imageI,axiom,(
    ! [H: hoare_1262092251_state > pname,F_17: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_17 )
     => ( finite_finite_pname @ ( image_202231862_pname @ H @ F_17 ) ) ) )).

thf(fact_32_finite__imageI,axiom,(
    ! [H: pname > pname,F_17: pname > $o] :
      ( ( finite_finite_pname @ F_17 )
     => ( finite_finite_pname @ ( image_pname_pname @ H @ F_17 ) ) ) )).

thf(fact_33_empty__subsetI,axiom,(
    ! [A_76: hoare_1262092251_state > $o] :
      ( ord_le870406270tate_o @ bot_bo113204042tate_o @ A_76 ) )).

thf(fact_34_empty__subsetI,axiom,(
    ! [A_76: ( pname > $o ) > $o] :
      ( ord_le1205211808me_o_o @ bot_bot_pname_o_o @ A_76 ) )).

thf(fact_35_empty__subsetI,axiom,(
    ! [A_76: ( hoare_1262092251_state > $o ) > $o] :
      ( ord_le2012720639te_o_o @ bot_bo1962689075te_o_o @ A_76 ) )).

thf(fact_36_empty__subsetI,axiom,(
    ! [A_76: pname > $o] :
      ( ord_less_eq_pname_o @ bot_bot_pname_o @ A_76 ) )).

thf(fact_37_finite_OinsertI,axiom,(
    ! [A_75: hoare_1262092251_state,A_74: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_74 )
     => ( finite1178804552_state @ ( insert81609953_state @ A_75 @ A_74 ) ) ) )).

thf(fact_38_finite_OinsertI,axiom,(
    ! [A_75: pname,A_74: pname > $o] :
      ( ( finite_finite_pname @ A_74 )
     => ( finite_finite_pname @ ( insert_pname @ A_75 @ A_74 ) ) ) )).

thf(fact_39_finite_OinsertI,axiom,(
    ! [A_75: ( pname > $o ) > $o,A_74: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_74 )
     => ( finite1066544169me_o_o @ ( insert_pname_o_o @ A_75 @ A_74 ) ) ) )).

thf(fact_40_finite_OinsertI,axiom,(
    ! [A_75: ( hoare_1262092251_state > $o ) > $o,A_74: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ A_74 )
     => ( finite1303896758te_o_o @ ( insert1691644879te_o_o @ A_75 @ A_74 ) ) ) )).

thf(fact_41_finite_OinsertI,axiom,(
    ! [A_75: hoare_1262092251_state > $o,A_74: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ A_74 )
     => ( finite1423311111tate_o @ ( insert1042460334tate_o @ A_75 @ A_74 ) ) ) )).

thf(fact_42_finite_OinsertI,axiom,(
    ! [A_75: pname > $o,A_74: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_74 )
     => ( finite297249702name_o @ ( insert_pname_o @ A_75 @ A_74 ) ) ) )).

thf(fact_43_finite_OemptyI,axiom,
    ( finite_finite_pname @ bot_bot_pname_o )).

thf(fact_44_finite_OemptyI,axiom,
    ( finite1178804552_state @ bot_bo113204042tate_o )).

thf(fact_45_finite_OemptyI,axiom,
    ( finite1066544169me_o_o @ bot_bot_pname_o_o_o )).

thf(fact_46_finite_OemptyI,axiom,
    ( finite1303896758te_o_o @ bot_bo388435036_o_o_o )).

thf(fact_47_finite_OemptyI,axiom,
    ( finite1423311111tate_o @ bot_bo1962689075te_o_o )).

thf(fact_48_finite_OemptyI,axiom,
    ( finite297249702name_o @ bot_bot_pname_o_o )).

thf(fact_49_finite__Collect__conjI,axiom,(
    ! [Q_1: pname > $o,P_9: pname > $o] :
      ( ( ( finite_finite_pname @ ( collect_pname @ P_9 ) )
        | ( finite_finite_pname @ ( collect_pname @ Q_1 ) ) )
     => ( finite_finite_pname
        @ ( collect_pname
          @ ^ [X_1: pname] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_50_finite__Collect__conjI,axiom,(
    ! [Q_1: hoare_1262092251_state > $o,P_9: hoare_1262092251_state > $o] :
      ( ( ( finite1178804552_state @ ( collec1121927558_state @ P_9 ) )
        | ( finite1178804552_state @ ( collec1121927558_state @ Q_1 ) ) )
     => ( finite1178804552_state
        @ ( collec1121927558_state
          @ ^ [X_1: hoare_1262092251_state] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_51_finite__Collect__conjI,axiom,(
    ! [Q_1: ( ( pname > $o ) > $o ) > $o,P_9: ( ( pname > $o ) > $o ) > $o] :
      ( ( ( finite1066544169me_o_o @ ( collect_pname_o_o @ P_9 ) )
        | ( finite1066544169me_o_o @ ( collect_pname_o_o @ Q_1 ) ) )
     => ( finite1066544169me_o_o
        @ ( collect_pname_o_o
          @ ^ [X_1: ( pname > $o ) > $o] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_52_finite__Collect__conjI,axiom,(
    ! [Q_1: ( ( hoare_1262092251_state > $o ) > $o ) > $o,P_9: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( ( finite1303896758te_o_o @ ( collec341954548te_o_o @ P_9 ) )
        | ( finite1303896758te_o_o @ ( collec341954548te_o_o @ Q_1 ) ) )
     => ( finite1303896758te_o_o
        @ ( collec341954548te_o_o
          @ ^ [X_1: ( hoare_1262092251_state > $o ) > $o] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_53_finite__Collect__conjI,axiom,(
    ! [Q_1: ( hoare_1262092251_state > $o ) > $o,P_9: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ( finite1423311111tate_o @ ( collec313158217tate_o @ P_9 ) )
        | ( finite1423311111tate_o @ ( collec313158217tate_o @ Q_1 ) ) )
     => ( finite1423311111tate_o
        @ ( collec313158217tate_o
          @ ^ [X_1: hoare_1262092251_state > $o] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_54_finite__Collect__conjI,axiom,(
    ! [Q_1: ( pname > $o ) > $o,P_9: ( pname > $o ) > $o] :
      ( ( ( finite297249702name_o @ ( collect_pname_o @ P_9 ) )
        | ( finite297249702name_o @ ( collect_pname_o @ Q_1 ) ) )
     => ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [X_1: pname > $o] :
              ( (&) @ ( P_9 @ X_1 ) @ ( Q_1 @ X_1 ) ) ) ) ) )).

thf(fact_55_image__constant__conv,axiom,(
    ! [C_8: hoare_1262092251_state,A_73: pname > $o] :
      ( ( ( A_73 = bot_bot_pname_o )
       => ( ( image_669833818_state
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = bot_bo113204042tate_o ) )
      & ( ( A_73 != bot_bot_pname_o )
       => ( ( image_669833818_state
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = ( insert81609953_state @ C_8 @ bot_bo113204042tate_o ) ) ) ) )).

thf(fact_56_image__constant__conv,axiom,(
    ! [C_8: pname,A_73: hoare_1262092251_state > $o] :
      ( ( ( A_73 = bot_bo113204042tate_o )
       => ( ( image_202231862_pname
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = bot_bot_pname_o ) )
      & ( ( A_73 != bot_bo113204042tate_o )
       => ( ( image_202231862_pname
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = ( insert_pname @ C_8 @ bot_bot_pname_o ) ) ) ) )).

thf(fact_57_image__constant__conv,axiom,(
    ! [C_8: pname > $o,A_73: hoare_1262092251_state > $o] :
      ( ( ( A_73 = bot_bo113204042tate_o )
       => ( ( image_1320925383name_o
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = bot_bot_pname_o_o ) )
      & ( ( A_73 != bot_bo113204042tate_o )
       => ( ( image_1320925383name_o
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = ( insert_pname_o @ C_8 @ bot_bot_pname_o_o ) ) ) ) )).

thf(fact_58_image__constant__conv,axiom,(
    ! [C_8: hoare_1262092251_state > $o,A_73: hoare_1262092251_state > $o] :
      ( ( ( A_73 = bot_bo113204042tate_o )
       => ( ( image_1403668518tate_o
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = bot_bo1962689075te_o_o ) )
      & ( ( A_73 != bot_bo113204042tate_o )
       => ( ( image_1403668518tate_o
            @ ^ [X_1: hoare_1262092251_state] : C_8
            @ A_73 )
          = ( insert1042460334tate_o @ C_8 @ bot_bo1962689075te_o_o ) ) ) ) )).

thf(fact_59_image__constant__conv,axiom,(
    ! [C_8: pname > $o,A_73: pname > $o] :
      ( ( ( A_73 = bot_bot_pname_o )
       => ( ( image_pname_pname_o
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = bot_bot_pname_o_o ) )
      & ( ( A_73 != bot_bot_pname_o )
       => ( ( image_pname_pname_o
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = ( insert_pname_o @ C_8 @ bot_bot_pname_o_o ) ) ) ) )).

thf(fact_60_image__constant__conv,axiom,(
    ! [C_8: hoare_1262092251_state > $o,A_73: pname > $o] :
      ( ( ( A_73 = bot_bot_pname_o )
       => ( ( image_518521461tate_o
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = bot_bo1962689075te_o_o ) )
      & ( ( A_73 != bot_bot_pname_o )
       => ( ( image_518521461tate_o
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = ( insert1042460334tate_o @ C_8 @ bot_bo1962689075te_o_o ) ) ) ) )).

thf(fact_61_image__constant__conv,axiom,(
    ! [C_8: pname,A_73: pname > $o] :
      ( ( ( A_73 = bot_bot_pname_o )
       => ( ( image_pname_pname
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = bot_bot_pname_o ) )
      & ( ( A_73 != bot_bot_pname_o )
       => ( ( image_pname_pname
            @ ^ [X_1: pname] : C_8
            @ A_73 )
          = ( insert_pname @ C_8 @ bot_bot_pname_o ) ) ) ) )).

thf(fact_62_image__constant__conv,axiom,(
    ! [C_8: hoare_1262092251_state,A_73: ( pname > $o ) > $o] :
      ( ( ( A_73 = bot_bot_pname_o_o )
       => ( ( image_1476171975_state
            @ ^ [X_1: pname > $o] : C_8
            @ A_73 )
          = bot_bo113204042tate_o ) )
      & ( ( A_73 != bot_bot_pname_o_o )
       => ( ( image_1476171975_state
            @ ^ [X_1: pname > $o] : C_8
            @ A_73 )
          = ( insert81609953_state @ C_8 @ bot_bo113204042tate_o ) ) ) ) )).

thf(fact_63_image__constant__conv,axiom,(
    ! [C_8: hoare_1262092251_state,A_73: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ( A_73 = bot_bo1962689075te_o_o )
       => ( ( image_234589002_state
            @ ^ [X_1: hoare_1262092251_state > $o] : C_8
            @ A_73 )
          = bot_bo113204042tate_o ) )
      & ( ( A_73 != bot_bo1962689075te_o_o )
       => ( ( image_234589002_state
            @ ^ [X_1: hoare_1262092251_state > $o] : C_8
            @ A_73 )
          = ( insert81609953_state @ C_8 @ bot_bo113204042tate_o ) ) ) ) )).

thf(fact_64_image__constant__conv,axiom,(
    ! [C_8: pname,A_73: ( pname > $o ) > $o] :
      ( ( ( A_73 = bot_bot_pname_o_o )
       => ( ( image_pname_o_pname
            @ ^ [X_1: pname > $o] : C_8
            @ A_73 )
          = bot_bot_pname_o ) )
      & ( ( A_73 != bot_bot_pname_o_o )
       => ( ( image_pname_o_pname
            @ ^ [X_1: pname > $o] : C_8
            @ A_73 )
          = ( insert_pname @ C_8 @ bot_bot_pname_o ) ) ) ) )).

thf(fact_65_image__constant__conv,axiom,(
    ! [C_8: pname,A_73: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ( A_73 = bot_bo1962689075te_o_o )
       => ( ( image_1820530197_pname
            @ ^ [X_1: hoare_1262092251_state > $o] : C_8
            @ A_73 )
          = bot_bot_pname_o ) )
      & ( ( A_73 != bot_bo1962689075te_o_o )
       => ( ( image_1820530197_pname
            @ ^ [X_1: hoare_1262092251_state > $o] : C_8
            @ A_73 )
          = ( insert_pname @ C_8 @ bot_bot_pname_o ) ) ) ) )).

thf(fact_66_image__constant,axiom,(
    ! [C_7: hoare_1262092251_state,X_18: pname,A_72: pname > $o] :
      ( ( member_pname @ X_18 @ A_72 )
     => ( ( image_669833818_state
          @ ^ [X_1: pname] : C_7
          @ A_72 )
        = ( insert81609953_state @ C_7 @ bot_bo113204042tate_o ) ) ) )).

thf(fact_67_image__constant,axiom,(
    ! [C_7: pname,X_18: hoare_1262092251_state,A_72: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ X_18 @ A_72 )
     => ( ( image_202231862_pname
          @ ^ [X_1: hoare_1262092251_state] : C_7
          @ A_72 )
        = ( insert_pname @ C_7 @ bot_bot_pname_o ) ) ) )).

thf(fact_68_image__constant,axiom,(
    ! [C_7: pname > $o,X_18: hoare_1262092251_state,A_72: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ X_18 @ A_72 )
     => ( ( image_1320925383name_o
          @ ^ [X_1: hoare_1262092251_state] : C_7
          @ A_72 )
        = ( insert_pname_o @ C_7 @ bot_bot_pname_o_o ) ) ) )).

thf(fact_69_image__constant,axiom,(
    ! [C_7: hoare_1262092251_state > $o,X_18: hoare_1262092251_state,A_72: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ X_18 @ A_72 )
     => ( ( image_1403668518tate_o
          @ ^ [X_1: hoare_1262092251_state] : C_7
          @ A_72 )
        = ( insert1042460334tate_o @ C_7 @ bot_bo1962689075te_o_o ) ) ) )).

thf(fact_70_image__constant,axiom,(
    ! [C_7: pname > $o,X_18: pname,A_72: pname > $o] :
      ( ( member_pname @ X_18 @ A_72 )
     => ( ( image_pname_pname_o
          @ ^ [X_1: pname] : C_7
          @ A_72 )
        = ( insert_pname_o @ C_7 @ bot_bot_pname_o_o ) ) ) )).

thf(fact_71_image__constant,axiom,(
    ! [C_7: hoare_1262092251_state > $o,X_18: pname,A_72: pname > $o] :
      ( ( member_pname @ X_18 @ A_72 )
     => ( ( image_518521461tate_o
          @ ^ [X_1: pname] : C_7
          @ A_72 )
        = ( insert1042460334tate_o @ C_7 @ bot_bo1962689075te_o_o ) ) ) )).

thf(fact_72_image__constant,axiom,(
    ! [C_7: pname,X_18: pname,A_72: pname > $o] :
      ( ( member_pname @ X_18 @ A_72 )
     => ( ( image_pname_pname
          @ ^ [X_1: pname] : C_7
          @ A_72 )
        = ( insert_pname @ C_7 @ bot_bot_pname_o ) ) ) )).

thf(fact_73_image__constant,axiom,(
    ! [C_7: hoare_1262092251_state,X_18: pname > $o,A_72: ( pname > $o ) > $o] :
      ( ( member_pname_o @ X_18 @ A_72 )
     => ( ( image_1476171975_state
          @ ^ [X_1: pname > $o] : C_7
          @ A_72 )
        = ( insert81609953_state @ C_7 @ bot_bo113204042tate_o ) ) ) )).

thf(fact_74_image__constant,axiom,(
    ! [C_7: hoare_1262092251_state,X_18: hoare_1262092251_state > $o,A_72: ( hoare_1262092251_state > $o ) > $o] :
      ( ( member907417095tate_o @ X_18 @ A_72 )
     => ( ( image_234589002_state
          @ ^ [X_1: hoare_1262092251_state > $o] : C_7
          @ A_72 )
        = ( insert81609953_state @ C_7 @ bot_bo113204042tate_o ) ) ) )).

thf(fact_75_image__constant,axiom,(
    ! [C_7: pname,X_18: pname > $o,A_72: ( pname > $o ) > $o] :
      ( ( member_pname_o @ X_18 @ A_72 )
     => ( ( image_pname_o_pname
          @ ^ [X_1: pname > $o] : C_7
          @ A_72 )
        = ( insert_pname @ C_7 @ bot_bot_pname_o ) ) ) )).

thf(fact_76_image__constant,axiom,(
    ! [C_7: pname,X_18: hoare_1262092251_state > $o,A_72: ( hoare_1262092251_state > $o ) > $o] :
      ( ( member907417095tate_o @ X_18 @ A_72 )
     => ( ( image_1820530197_pname
          @ ^ [X_1: hoare_1262092251_state > $o] : C_7
          @ A_72 )
        = ( insert_pname @ C_7 @ bot_bot_pname_o ) ) ) )).

thf(fact_77_insert__dom,axiom,(
    ! [F_16: pname > option_com,X_17: pname,Y_4: com] :
      ( ( ( F_16 @ X_17 )
        = ( some_com @ Y_4 ) )
     => ( ( insert_pname @ X_17 @ ( dom_pname_com @ F_16 ) )
        = ( dom_pname_com @ F_16 ) ) ) )).

thf(fact_78_insert__dom,axiom,(
    ! [F_16: ( pname > $o ) > option_com,X_17: pname > $o,Y_4: com] :
      ( ( ( F_16 @ X_17 )
        = ( some_com @ Y_4 ) )
     => ( ( insert_pname_o @ X_17 @ ( dom_pname_o_com @ F_16 ) )
        = ( dom_pname_o_com @ F_16 ) ) ) )).

thf(fact_79_insert__dom,axiom,(
    ! [F_16: ( hoare_1262092251_state > $o ) > option_com,X_17: hoare_1262092251_state > $o,Y_4: com] :
      ( ( ( F_16 @ X_17 )
        = ( some_com @ Y_4 ) )
     => ( ( insert1042460334tate_o @ X_17 @ ( dom_Ho1489634536_o_com @ F_16 ) )
        = ( dom_Ho1489634536_o_com @ F_16 ) ) ) )).

thf(fact_80_finite__surj,axiom,(
    ! [B_40: hoare_1262092251_state > $o,F_15: pname > hoare_1262092251_state,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_le870406270tate_o @ B_40 @ ( image_669833818_state @ F_15 @ A_71 ) )
       => ( finite1178804552_state @ B_40 ) ) ) )).

thf(fact_81_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: ( ( pname > $o ) > $o ) > pname,A_71: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_471733107_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_82_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: ( ( hoare_1262092251_state > $o ) > $o ) > pname,A_71: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_893364936_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_83_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: ( hoare_1262092251_state > $o ) > pname,A_71: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_1820530197_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_84_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: ( pname > $o ) > pname,A_71: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_pname_o_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_85_finite__surj,axiom,(
    ! [B_40: hoare_1262092251_state > $o,F_15: ( ( pname > $o ) > $o ) > hoare_1262092251_state,A_71: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_71 )
     => ( ( ord_le870406270tate_o @ B_40 @ ( image_1036078444_state @ F_15 @ A_71 ) )
       => ( finite1178804552_state @ B_40 ) ) ) )).

thf(fact_86_finite__surj,axiom,(
    ! [B_40: hoare_1262092251_state > $o,F_15: ( ( hoare_1262092251_state > $o ) > $o ) > hoare_1262092251_state,A_71: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( finite1303896758te_o_o @ A_71 )
     => ( ( ord_le870406270tate_o @ B_40 @ ( image_165349207_state @ F_15 @ A_71 ) )
       => ( finite1178804552_state @ B_40 ) ) ) )).

thf(fact_87_finite__surj,axiom,(
    ! [B_40: hoare_1262092251_state > $o,F_15: ( hoare_1262092251_state > $o ) > hoare_1262092251_state,A_71: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ A_71 )
     => ( ( ord_le870406270tate_o @ B_40 @ ( image_234589002_state @ F_15 @ A_71 ) )
       => ( finite1178804552_state @ B_40 ) ) ) )).

thf(fact_88_finite__surj,axiom,(
    ! [B_40: hoare_1262092251_state > $o,F_15: ( pname > $o ) > hoare_1262092251_state,A_71: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_71 )
     => ( ( ord_le870406270tate_o @ B_40 @ ( image_1476171975_state @ F_15 @ A_71 ) )
       => ( finite1178804552_state @ B_40 ) ) ) )).

thf(fact_89_finite__surj,axiom,(
    ! [B_40: ( ( pname > $o ) > $o ) > $o,F_15: pname > ( pname > $o ) > $o,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_le1828183645_o_o_o @ B_40 @ ( image_504089495me_o_o @ F_15 @ A_71 ) )
       => ( finite1066544169me_o_o @ B_40 ) ) ) )).

thf(fact_90_finite__surj,axiom,(
    ! [B_40: ( ( hoare_1262092251_state > $o ) > $o ) > $o,F_15: pname > ( hoare_1262092251_state > $o ) > $o,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_le1891858320_o_o_o @ B_40 @ ( image_827868872te_o_o @ F_15 @ A_71 ) )
       => ( finite1303896758te_o_o @ B_40 ) ) ) )).

thf(fact_91_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: pname > pname,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_pname_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_92_finite__surj,axiom,(
    ! [B_40: ( hoare_1262092251_state > $o ) > $o,F_15: pname > hoare_1262092251_state > $o,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_le2012720639te_o_o @ B_40 @ ( image_518521461tate_o @ F_15 @ A_71 ) )
       => ( finite1423311111tate_o @ B_40 ) ) ) )).

thf(fact_93_finite__surj,axiom,(
    ! [B_40: ( pname > $o ) > $o,F_15: pname > pname > $o,A_71: pname > $o] :
      ( ( finite_finite_pname @ A_71 )
     => ( ( ord_le1205211808me_o_o @ B_40 @ ( image_pname_pname_o @ F_15 @ A_71 ) )
       => ( finite297249702name_o @ B_40 ) ) ) )).

thf(fact_94_finite__surj,axiom,(
    ! [B_40: ( ( pname > $o ) > $o ) > $o,F_15: hoare_1262092251_state > ( pname > $o ) > $o,A_71: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_71 )
     => ( ( ord_le1828183645_o_o_o @ B_40 @ ( image_333245000me_o_o @ F_15 @ A_71 ) )
       => ( finite1066544169me_o_o @ B_40 ) ) ) )).

thf(fact_95_finite__surj,axiom,(
    ! [B_40: ( ( hoare_1262092251_state > $o ) > $o ) > $o,F_15: hoare_1262092251_state > ( hoare_1262092251_state > $o ) > $o,A_71: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_71 )
     => ( ( ord_le1891858320_o_o_o @ B_40 @ ( image_1731108951te_o_o @ F_15 @ A_71 ) )
       => ( finite1303896758te_o_o @ B_40 ) ) ) )).

thf(fact_96_finite__surj,axiom,(
    ! [B_40: pname > $o,F_15: hoare_1262092251_state > pname,A_71: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_71 )
     => ( ( ord_less_eq_pname_o @ B_40 @ ( image_202231862_pname @ F_15 @ A_71 ) )
       => ( finite_finite_pname @ B_40 ) ) ) )).

thf(fact_97_finite__surj,axiom,(
    ! [B_40: ( hoare_1262092251_state > $o ) > $o,F_15: hoare_1262092251_state > hoare_1262092251_state > $o,A_71: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_71 )
     => ( ( ord_le2012720639te_o_o @ B_40 @ ( image_1403668518tate_o @ F_15 @ A_71 ) )
       => ( finite1423311111tate_o @ B_40 ) ) ) )).

thf(fact_98_finite__surj,axiom,(
    ! [B_40: ( pname > $o ) > $o,F_15: hoare_1262092251_state > pname > $o,A_71: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ A_71 )
     => ( ( ord_le1205211808me_o_o @ B_40 @ ( image_1320925383name_o @ F_15 @ A_71 ) )
       => ( finite297249702name_o @ B_40 ) ) ) )).

thf(fact_99_subset__singletonD,axiom,(
    ! [A_70: hoare_1262092251_state > $o,X_16: hoare_1262092251_state] :
      ( ( ord_le870406270tate_o @ A_70 @ ( insert81609953_state @ X_16 @ bot_bo113204042tate_o ) )
     => ( ( A_70 = bot_bo113204042tate_o )
        | ( A_70
          = ( insert81609953_state @ X_16 @ bot_bo113204042tate_o ) ) ) ) )).

thf(fact_100_subset__singletonD,axiom,(
    ! [A_70: ( pname > $o ) > $o,X_16: pname > $o] :
      ( ( ord_le1205211808me_o_o @ A_70 @ ( insert_pname_o @ X_16 @ bot_bot_pname_o_o ) )
     => ( ( A_70 = bot_bot_pname_o_o )
        | ( A_70
          = ( insert_pname_o @ X_16 @ bot_bot_pname_o_o ) ) ) ) )).

thf(fact_101_subset__singletonD,axiom,(
    ! [A_70: ( hoare_1262092251_state > $o ) > $o,X_16: hoare_1262092251_state > $o] :
      ( ( ord_le2012720639te_o_o @ A_70 @ ( insert1042460334tate_o @ X_16 @ bot_bo1962689075te_o_o ) )
     => ( ( A_70 = bot_bo1962689075te_o_o )
        | ( A_70
          = ( insert1042460334tate_o @ X_16 @ bot_bo1962689075te_o_o ) ) ) ) )).

thf(fact_102_subset__singletonD,axiom,(
    ! [A_70: pname > $o,X_16: pname] :
      ( ( ord_less_eq_pname_o @ A_70 @ ( insert_pname @ X_16 @ bot_bot_pname_o ) )
     => ( ( A_70 = bot_bot_pname_o )
        | ( A_70
          = ( insert_pname @ X_16 @ bot_bot_pname_o ) ) ) ) )).

thf(fact_103_MGF,axiom,(
    ! [C_1: com] :
      ( hoare_1821564147gleton
     => ( wT_bodies
       => ( ( wt @ C_1 )
         => ( hoare_930741239_state @ bot_bo113204042tate_o @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ C_1 ) @ bot_bo113204042tate_o ) ) ) ) ) )).

thf(fact_104_emptyE,axiom,(
    ! [A_69: hoare_1262092251_state] :
      ~ ( member5164104_state @ A_69 @ bot_bo113204042tate_o ) )).

thf(fact_105_emptyE,axiom,(
    ! [A_69: pname > $o] :
      ~ ( member_pname_o @ A_69 @ bot_bot_pname_o_o ) )).

thf(fact_106_emptyE,axiom,(
    ! [A_69: hoare_1262092251_state > $o] :
      ~ ( member907417095tate_o @ A_69 @ bot_bo1962689075te_o_o ) )).

thf(fact_107_emptyE,axiom,(
    ! [A_69: pname] :
      ~ ( member_pname @ A_69 @ bot_bot_pname_o ) )).

thf(fact_108_insertCI,axiom,(
    ! [B_39: hoare_1262092251_state,A_68: hoare_1262092251_state,B_38: hoare_1262092251_state > $o] :
      ( ( ~ ( member5164104_state @ A_68 @ B_38 )
       => ( A_68 = B_39 ) )
     => ( member5164104_state @ A_68 @ ( insert81609953_state @ B_39 @ B_38 ) ) ) )).

thf(fact_109_insertCI,axiom,(
    ! [B_39: pname > $o,A_68: pname > $o,B_38: ( pname > $o ) > $o] :
      ( ( ~ ( member_pname_o @ A_68 @ B_38 )
       => ( A_68 = B_39 ) )
     => ( member_pname_o @ A_68 @ ( insert_pname_o @ B_39 @ B_38 ) ) ) )).

thf(fact_110_insertCI,axiom,(
    ! [B_39: hoare_1262092251_state > $o,A_68: hoare_1262092251_state > $o,B_38: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ~ ( member907417095tate_o @ A_68 @ B_38 )
       => ( A_68 = B_39 ) )
     => ( member907417095tate_o @ A_68 @ ( insert1042460334tate_o @ B_39 @ B_38 ) ) ) )).

thf(fact_111_insertCI,axiom,(
    ! [B_39: pname,A_68: pname,B_38: pname > $o] :
      ( ( ~ ( member_pname @ A_68 @ B_38 )
       => ( A_68 = B_39 ) )
     => ( member_pname @ A_68 @ ( insert_pname @ B_39 @ B_38 ) ) ) )).

thf(fact_112_insertE,axiom,(
    ! [A_67: hoare_1262092251_state,B_37: hoare_1262092251_state,A_66: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ A_67 @ ( insert81609953_state @ B_37 @ A_66 ) )
     => ( ( A_67 != B_37 )
       => ( member5164104_state @ A_67 @ A_66 ) ) ) )).

thf(fact_113_insertE,axiom,(
    ! [A_67: pname > $o,B_37: pname > $o,A_66: ( pname > $o ) > $o] :
      ( ( member_pname_o @ A_67 @ ( insert_pname_o @ B_37 @ A_66 ) )
     => ( ( A_67 != B_37 )
       => ( member_pname_o @ A_67 @ A_66 ) ) ) )).

thf(fact_114_insertE,axiom,(
    ! [A_67: hoare_1262092251_state > $o,B_37: hoare_1262092251_state > $o,A_66: ( hoare_1262092251_state > $o ) > $o] :
      ( ( member907417095tate_o @ A_67 @ ( insert1042460334tate_o @ B_37 @ A_66 ) )
     => ( ( A_67 != B_37 )
       => ( member907417095tate_o @ A_67 @ A_66 ) ) ) )).

thf(fact_115_insertE,axiom,(
    ! [A_67: pname,B_37: pname,A_66: pname > $o] :
      ( ( member_pname @ A_67 @ ( insert_pname @ B_37 @ A_66 ) )
     => ( ( A_67 != B_37 )
       => ( member_pname @ A_67 @ A_66 ) ) ) )).

thf(fact_116_equalityI,axiom,(
    ! [A_65: hoare_1262092251_state > $o,B_36: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_65 @ B_36 )
     => ( ( ord_le870406270tate_o @ B_36 @ A_65 )
       => ( A_65 = B_36 ) ) ) )).

thf(fact_117_equalityI,axiom,(
    ! [A_65: ( pname > $o ) > $o,B_36: ( pname > $o ) > $o] :
      ( ( ord_le1205211808me_o_o @ A_65 @ B_36 )
     => ( ( ord_le1205211808me_o_o @ B_36 @ A_65 )
       => ( A_65 = B_36 ) ) ) )).

thf(fact_118_equalityI,axiom,(
    ! [A_65: ( hoare_1262092251_state > $o ) > $o,B_36: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ord_le2012720639te_o_o @ A_65 @ B_36 )
     => ( ( ord_le2012720639te_o_o @ B_36 @ A_65 )
       => ( A_65 = B_36 ) ) ) )).

thf(fact_119_equalityI,axiom,(
    ! [A_65: pname > $o,B_36: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_65 @ B_36 )
     => ( ( ord_less_eq_pname_o @ B_36 @ A_65 )
       => ( A_65 = B_36 ) ) ) )).

thf(fact_120_subsetD,axiom,(
    ! [C_6: hoare_1262092251_state,A_64: hoare_1262092251_state > $o,B_35: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_64 @ B_35 )
     => ( ( member5164104_state @ C_6 @ A_64 )
       => ( member5164104_state @ C_6 @ B_35 ) ) ) )).

thf(fact_121_subsetD,axiom,(
    ! [C_6: pname > $o,A_64: ( pname > $o ) > $o,B_35: ( pname > $o ) > $o] :
      ( ( ord_le1205211808me_o_o @ A_64 @ B_35 )
     => ( ( member_pname_o @ C_6 @ A_64 )
       => ( member_pname_o @ C_6 @ B_35 ) ) ) )).

thf(fact_122_subsetD,axiom,(
    ! [C_6: hoare_1262092251_state > $o,A_64: ( hoare_1262092251_state > $o ) > $o,B_35: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ord_le2012720639te_o_o @ A_64 @ B_35 )
     => ( ( member907417095tate_o @ C_6 @ A_64 )
       => ( member907417095tate_o @ C_6 @ B_35 ) ) ) )).

thf(fact_123_subsetD,axiom,(
    ! [C_6: pname,A_64: pname > $o,B_35: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_64 @ B_35 )
     => ( ( member_pname @ C_6 @ A_64 )
       => ( member_pname @ C_6 @ B_35 ) ) ) )).

thf(fact_124_image__eqI,axiom,(
    ! [A_63: hoare_1262092251_state > $o,B_34: pname > $o,F_14: hoare_1262092251_state > pname > $o,X_15: hoare_1262092251_state] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member5164104_state @ X_15 @ A_63 )
       => ( member_pname_o @ B_34 @ ( image_1320925383name_o @ F_14 @ A_63 ) ) ) ) )).

thf(fact_125_image__eqI,axiom,(
    ! [A_63: hoare_1262092251_state > $o,B_34: hoare_1262092251_state > $o,F_14: hoare_1262092251_state > hoare_1262092251_state > $o,X_15: hoare_1262092251_state] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member5164104_state @ X_15 @ A_63 )
       => ( member907417095tate_o @ B_34 @ ( image_1403668518tate_o @ F_14 @ A_63 ) ) ) ) )).

thf(fact_126_image__eqI,axiom,(
    ! [A_63: pname > $o,B_34: pname > $o,F_14: pname > pname > $o,X_15: pname] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname @ X_15 @ A_63 )
       => ( member_pname_o @ B_34 @ ( image_pname_pname_o @ F_14 @ A_63 ) ) ) ) )).

thf(fact_127_image__eqI,axiom,(
    ! [A_63: pname > $o,B_34: hoare_1262092251_state > $o,F_14: pname > hoare_1262092251_state > $o,X_15: pname] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname @ X_15 @ A_63 )
       => ( member907417095tate_o @ B_34 @ ( image_518521461tate_o @ F_14 @ A_63 ) ) ) ) )).

thf(fact_128_image__eqI,axiom,(
    ! [A_63: ( pname > $o ) > $o,B_34: hoare_1262092251_state,F_14: ( pname > $o ) > hoare_1262092251_state,X_15: pname > $o] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname_o @ X_15 @ A_63 )
       => ( member5164104_state @ B_34 @ ( image_1476171975_state @ F_14 @ A_63 ) ) ) ) )).

thf(fact_129_image__eqI,axiom,(
    ! [A_63: ( hoare_1262092251_state > $o ) > $o,B_34: hoare_1262092251_state,F_14: ( hoare_1262092251_state > $o ) > hoare_1262092251_state,X_15: hoare_1262092251_state > $o] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member907417095tate_o @ X_15 @ A_63 )
       => ( member5164104_state @ B_34 @ ( image_234589002_state @ F_14 @ A_63 ) ) ) ) )).

thf(fact_130_image__eqI,axiom,(
    ! [A_63: hoare_1262092251_state > $o,B_34: pname,F_14: hoare_1262092251_state > pname,X_15: hoare_1262092251_state] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member5164104_state @ X_15 @ A_63 )
       => ( member_pname @ B_34 @ ( image_202231862_pname @ F_14 @ A_63 ) ) ) ) )).

thf(fact_131_image__eqI,axiom,(
    ! [A_63: pname > $o,B_34: pname,F_14: pname > pname,X_15: pname] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname @ X_15 @ A_63 )
       => ( member_pname @ B_34 @ ( image_pname_pname @ F_14 @ A_63 ) ) ) ) )).

thf(fact_132_image__eqI,axiom,(
    ! [A_63: ( pname > $o ) > $o,B_34: pname,F_14: ( pname > $o ) > pname,X_15: pname > $o] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname_o @ X_15 @ A_63 )
       => ( member_pname @ B_34 @ ( image_pname_o_pname @ F_14 @ A_63 ) ) ) ) )).

thf(fact_133_image__eqI,axiom,(
    ! [A_63: ( hoare_1262092251_state > $o ) > $o,B_34: pname,F_14: ( hoare_1262092251_state > $o ) > pname,X_15: hoare_1262092251_state > $o] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member907417095tate_o @ X_15 @ A_63 )
       => ( member_pname @ B_34 @ ( image_1820530197_pname @ F_14 @ A_63 ) ) ) ) )).

thf(fact_134_image__eqI,axiom,(
    ! [A_63: pname > $o,B_34: hoare_1262092251_state,F_14: pname > hoare_1262092251_state,X_15: pname] :
      ( ( B_34
        = ( F_14 @ X_15 ) )
     => ( ( member_pname @ X_15 @ A_63 )
       => ( member5164104_state @ B_34 @ ( image_669833818_state @ F_14 @ A_63 ) ) ) ) )).

thf(fact_135_equals0D,axiom,(
    ! [A_62: pname > $o,A_61: ( pname > $o ) > $o] :
      ( ( A_61 = bot_bot_pname_o_o )
     => ~ ( member_pname_o @ A_62 @ A_61 ) ) )).

thf(fact_136_equals0D,axiom,(
    ! [A_62: hoare_1262092251_state > $o,A_61: ( hoare_1262092251_state > $o ) > $o] :
      ( ( A_61 = bot_bo1962689075te_o_o )
     => ~ ( member907417095tate_o @ A_62 @ A_61 ) ) )).

thf(fact_137_equals0D,axiom,(
    ! [A_62: hoare_1262092251_state,A_61: hoare_1262092251_state > $o] :
      ( ( A_61 = bot_bo113204042tate_o )
     => ~ ( member5164104_state @ A_62 @ A_61 ) ) )).

thf(fact_138_equals0D,axiom,(
    ! [A_62: pname,A_61: pname > $o] :
      ( ( A_61 = bot_bot_pname_o )
     => ~ ( member_pname @ A_62 @ A_61 ) ) )).

thf(fact_139_Collect__empty__eq,axiom,(
    ! [P_8: ( ( pname > $o ) > $o ) > $o] :
      ( ( ( collect_pname_o_o @ P_8 )
        = bot_bot_pname_o_o_o )
    <=> ! [X_1: ( pname > $o ) > $o] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_140_Collect__empty__eq,axiom,(
    ! [P_8: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( ( collec341954548te_o_o @ P_8 )
        = bot_bo388435036_o_o_o )
    <=> ! [X_1: ( hoare_1262092251_state > $o ) > $o] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_141_Collect__empty__eq,axiom,(
    ! [P_8: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ( collec313158217tate_o @ P_8 )
        = bot_bo1962689075te_o_o )
    <=> ! [X_1: hoare_1262092251_state > $o] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_142_Collect__empty__eq,axiom,(
    ! [P_8: ( pname > $o ) > $o] :
      ( ( ( collect_pname_o @ P_8 )
        = bot_bot_pname_o_o )
    <=> ! [X_1: pname > $o] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_143_Collect__empty__eq,axiom,(
    ! [P_8: hoare_1262092251_state > $o] :
      ( ( ( collec1121927558_state @ P_8 )
        = bot_bo113204042tate_o )
    <=> ! [X_1: hoare_1262092251_state] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_144_Collect__empty__eq,axiom,(
    ! [P_8: pname > $o] :
      ( ( ( collect_pname @ P_8 )
        = bot_bot_pname_o )
    <=> ! [X_1: pname] :
          ~ ( P_8 @ X_1 ) ) )).

thf(fact_145_empty__iff,axiom,(
    ! [C_5: pname > $o] :
      ~ ( member_pname_o @ C_5 @ bot_bot_pname_o_o ) )).

thf(fact_146_empty__iff,axiom,(
    ! [C_5: hoare_1262092251_state > $o] :
      ~ ( member907417095tate_o @ C_5 @ bot_bo1962689075te_o_o ) )).

thf(fact_147_empty__iff,axiom,(
    ! [C_5: hoare_1262092251_state] :
      ~ ( member5164104_state @ C_5 @ bot_bo113204042tate_o ) )).

thf(fact_148_empty__iff,axiom,(
    ! [C_5: pname] :
      ~ ( member_pname @ C_5 @ bot_bot_pname_o ) )).

thf(fact_149_empty__Collect__eq,axiom,(
    ! [P_7: ( ( pname > $o ) > $o ) > $o] :
      ( ( bot_bot_pname_o_o_o
        = ( collect_pname_o_o @ P_7 ) )
    <=> ! [X_1: ( pname > $o ) > $o] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_150_empty__Collect__eq,axiom,(
    ! [P_7: ( ( hoare_1262092251_state > $o ) > $o ) > $o] :
      ( ( bot_bo388435036_o_o_o
        = ( collec341954548te_o_o @ P_7 ) )
    <=> ! [X_1: ( hoare_1262092251_state > $o ) > $o] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_151_empty__Collect__eq,axiom,(
    ! [P_7: ( hoare_1262092251_state > $o ) > $o] :
      ( ( bot_bo1962689075te_o_o
        = ( collec313158217tate_o @ P_7 ) )
    <=> ! [X_1: hoare_1262092251_state > $o] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_152_empty__Collect__eq,axiom,(
    ! [P_7: ( pname > $o ) > $o] :
      ( ( bot_bot_pname_o_o
        = ( collect_pname_o @ P_7 ) )
    <=> ! [X_1: pname > $o] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_153_empty__Collect__eq,axiom,(
    ! [P_7: hoare_1262092251_state > $o] :
      ( ( bot_bo113204042tate_o
        = ( collec1121927558_state @ P_7 ) )
    <=> ! [X_1: hoare_1262092251_state] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_154_empty__Collect__eq,axiom,(
    ! [P_7: pname > $o] :
      ( ( bot_bot_pname_o
        = ( collect_pname @ P_7 ) )
    <=> ! [X_1: pname] :
          ~ ( P_7 @ X_1 ) ) )).

thf(fact_155_ex__in__conv,axiom,(
    ! [A_60: ( pname > $o ) > $o] :
      ( ? [X_1: pname > $o] :
          ( member_pname_o @ X_1 @ A_60 )
    <=> ( A_60 != bot_bot_pname_o_o ) ) )).

thf(fact_156_ex__in__conv,axiom,(
    ! [A_60: ( hoare_1262092251_state > $o ) > $o] :
      ( ? [X_1: hoare_1262092251_state > $o] :
          ( member907417095tate_o @ X_1 @ A_60 )
    <=> ( A_60 != bot_bo1962689075te_o_o ) ) )).

thf(fact_157_ex__in__conv,axiom,(
    ! [A_60: hoare_1262092251_state > $o] :
      ( ? [X_1: hoare_1262092251_state] :
          ( member5164104_state @ X_1 @ A_60 )
    <=> ( A_60 != bot_bo113204042tate_o ) ) )).

thf(fact_158_ex__in__conv,axiom,(
    ! [A_60: pname > $o] :
      ( ? [X_1: pname] :
          ( member_pname @ X_1 @ A_60 )
    <=> ( A_60 != bot_bot_pname_o ) ) )).

thf(fact_159_all__not__in__conv,axiom,(
    ! [A_59: ( pname > $o ) > $o] :
      ( ! [X_1: pname > $o] :
          ~ ( member_pname_o @ X_1 @ A_59 )
    <=> ( A_59 = bot_bot_pname_o_o ) ) )).

thf(fact_160_all__not__in__conv,axiom,(
    ! [A_59: ( hoare_1262092251_state > $o ) > $o] :
      ( ! [X_1: hoare_1262092251_state > $o] :
          ~ ( member907417095tate_o @ X_1 @ A_59 )
    <=> ( A_59 = bot_bo1962689075te_o_o ) ) )).

thf(fact_161_all__not__in__conv,axiom,(
    ! [A_59: hoare_1262092251_state > $o] :
      ( ! [X_1: hoare_1262092251_state] :
          ~ ( member5164104_state @ X_1 @ A_59 )
    <=> ( A_59 = bot_bo113204042tate_o ) ) )).

thf(fact_162_all__not__in__conv,axiom,(
    ! [A_59: pname > $o] :
      ( ! [X_1: pname] :
          ~ ( member_pname @ X_1 @ A_59 )
    <=> ( A_59 = bot_bot_pname_o ) ) )).

thf(fact_163_empty__def,axiom,
    ( bot_bo388435036_o_o_o
    = ( collec341954548te_o_o
      @ ^ [X_1: ( hoare_1262092251_state > $o ) > $o] : $false ) )).

thf(fact_164_empty__def,axiom,
    ( bot_bo1962689075te_o_o
    = ( collec313158217tate_o
      @ ^ [X_1: hoare_1262092251_state > $o] : $false ) )).

thf(fact_165_empty__def,axiom,
    ( bot_bot_pname_o_o
    = ( collect_pname_o
      @ ^ [X_1: pname > $o] : $false ) )).

thf(fact_166_empty__def,axiom,
    ( bot_bo113204042tate_o
    = ( collec1121927558_state
      @ ^ [X_1: hoare_1262092251_state] : $false ) )).

thf(fact_167_empty__def,axiom,
    ( bot_bot_pname_o
    = ( collect_pname
      @ ^ [X_1: pname] : $false ) )).

thf(fact_168_insert__absorb,axiom,(
    ! [A_58: pname,A_57: pname > $o] :
      ( ( member_pname @ A_58 @ A_57 )
     => ( ( insert_pname @ A_58 @ A_57 )
        = A_57 ) ) )).

thf(fact_169_insert__absorb,axiom,(
    ! [A_58: hoare_1262092251_state,A_57: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ A_58 @ A_57 )
     => ( ( insert81609953_state @ A_58 @ A_57 )
        = A_57 ) ) )).

thf(fact_170_insertI2,axiom,(
    ! [B_33: pname,A_56: pname,B_32: pname > $o] :
      ( ( member_pname @ A_56 @ B_32 )
     => ( member_pname @ A_56 @ ( insert_pname @ B_33 @ B_32 ) ) ) )).

thf(fact_171_insertI2,axiom,(
    ! [B_33: hoare_1262092251_state,A_56: hoare_1262092251_state,B_32: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ A_56 @ B_32 )
     => ( member5164104_state @ A_56 @ ( insert81609953_state @ B_33 @ B_32 ) ) ) )).

thf(fact_172_insert__ident,axiom,(
    ! [B_31: pname > $o,X_14: pname,A_55: pname > $o] :
      ( ~ ( member_pname @ X_14 @ A_55 )
     => ( ~ ( member_pname @ X_14 @ B_31 )
       => ( ( ( insert_pname @ X_14 @ A_55 )
            = ( insert_pname @ X_14 @ B_31 ) )
        <=> ( A_55 = B_31 ) ) ) ) )).

thf(fact_173_insert__ident,axiom,(
    ! [B_31: hoare_1262092251_state > $o,X_14: hoare_1262092251_state,A_55: hoare_1262092251_state > $o] :
      ( ~ ( member5164104_state @ X_14 @ A_55 )
     => ( ~ ( member5164104_state @ X_14 @ B_31 )
       => ( ( ( insert81609953_state @ X_14 @ A_55 )
            = ( insert81609953_state @ X_14 @ B_31 ) )
        <=> ( A_55 = B_31 ) ) ) ) )).

thf(fact_174_insert__code,axiom,(
    ! [Y_3: pname,A_54: pname > $o,X_13: pname] :
      ( ( insert_pname @ Y_3 @ A_54 @ X_13 )
    <=> ( ( Y_3 = X_13 )
        | ( A_54 @ X_13 ) ) ) )).

thf(fact_175_insert__code,axiom,(
    ! [Y_3: hoare_1262092251_state,A_54: hoare_1262092251_state > $o,X_13: hoare_1262092251_state] :
      ( ( insert81609953_state @ Y_3 @ A_54 @ X_13 )
    <=> ( ( Y_3 = X_13 )
        | ( A_54 @ X_13 ) ) ) )).

thf(fact_176_insert__iff,axiom,(
    ! [A_53: pname,B_30: pname,A_52: pname > $o] :
      ( ( member_pname @ A_53 @ ( insert_pname @ B_30 @ A_52 ) )
    <=> ( ( A_53 = B_30 )
        | ( member_pname @ A_53 @ A_52 ) ) ) )).

thf(fact_177_insert__iff,axiom,(
    ! [A_53: hoare_1262092251_state,B_30: hoare_1262092251_state,A_52: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ A_53 @ ( insert81609953_state @ B_30 @ A_52 ) )
    <=> ( ( A_53 = B_30 )
        | ( member5164104_state @ A_53 @ A_52 ) ) ) )).

thf(fact_178_insert__commute,axiom,(
    ! [X_12: pname,Y_2: pname,A_51: pname > $o] :
      ( ( insert_pname @ X_12 @ ( insert_pname @ Y_2 @ A_51 ) )
      = ( insert_pname @ Y_2 @ ( insert_pname @ X_12 @ A_51 ) ) ) )).

thf(fact_179_insert__commute,axiom,(
    ! [X_12: hoare_1262092251_state,Y_2: hoare_1262092251_state,A_51: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ X_12 @ ( insert81609953_state @ Y_2 @ A_51 ) )
      = ( insert81609953_state @ Y_2 @ ( insert81609953_state @ X_12 @ A_51 ) ) ) )).

thf(fact_180_insert__absorb2,axiom,(
    ! [X_11: pname,A_50: pname > $o] :
      ( ( insert_pname @ X_11 @ ( insert_pname @ X_11 @ A_50 ) )
      = ( insert_pname @ X_11 @ A_50 ) ) )).

thf(fact_181_insert__absorb2,axiom,(
    ! [X_11: hoare_1262092251_state,A_50: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ X_11 @ ( insert81609953_state @ X_11 @ A_50 ) )
      = ( insert81609953_state @ X_11 @ A_50 ) ) )).

thf(fact_182_insert__Collect,axiom,(
    ! [A_49: pname,P_6: pname > $o] :
      ( ( insert_pname @ A_49 @ ( collect_pname @ P_6 ) )
      = ( collect_pname
        @ ^ [U: pname] :
            ( (=>) @ ( (~) @ ( U = A_49 ) ) @ ( P_6 @ U ) ) ) ) )).

thf(fact_183_insert__Collect,axiom,(
    ! [A_49: hoare_1262092251_state,P_6: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ A_49 @ ( collec1121927558_state @ P_6 ) )
      = ( collec1121927558_state
        @ ^ [U: hoare_1262092251_state] :
            ( (=>) @ ( (~) @ ( U = A_49 ) ) @ ( P_6 @ U ) ) ) ) )).

thf(fact_184_insert__Collect,axiom,(
    ! [A_49: pname > $o,P_6: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ A_49 @ ( collect_pname_o @ P_6 ) )
      = ( collect_pname_o
        @ ^ [U: pname > $o] :
            ( (=>) @ ( (~) @ ( U = A_49 ) ) @ ( P_6 @ U ) ) ) ) )).

thf(fact_185_insert__Collect,axiom,(
    ! [A_49: hoare_1262092251_state > $o,P_6: ( hoare_1262092251_state > $o ) > $o] :
      ( ( insert1042460334tate_o @ A_49 @ ( collec313158217tate_o @ P_6 ) )
      = ( collec313158217tate_o
        @ ^ [U: hoare_1262092251_state > $o] :
            ( (=>) @ ( (~) @ ( U = A_49 ) ) @ ( P_6 @ U ) ) ) ) )).

thf(fact_186_insert__compr,axiom,(
    ! [A_48: pname,B_29: pname > $o] :
      ( ( insert_pname @ A_48 @ B_29 )
      = ( collect_pname
        @ ^ [X_1: pname] :
            ( (|) @ ( X_1 = A_48 ) @ ( member_pname @ X_1 @ B_29 ) ) ) ) )).

thf(fact_187_insert__compr,axiom,(
    ! [A_48: hoare_1262092251_state,B_29: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ A_48 @ B_29 )
      = ( collec1121927558_state
        @ ^ [X_1: hoare_1262092251_state] :
            ( (|) @ ( X_1 = A_48 ) @ ( member5164104_state @ X_1 @ B_29 ) ) ) ) )).

thf(fact_188_insert__compr,axiom,(
    ! [A_48: pname > $o,B_29: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ A_48 @ B_29 )
      = ( collect_pname_o
        @ ^ [X_1: pname > $o] :
            ( (|) @ ( X_1 = A_48 ) @ ( member_pname_o @ X_1 @ B_29 ) ) ) ) )).

thf(fact_189_insert__compr,axiom,(
    ! [A_48: hoare_1262092251_state > $o,B_29: ( hoare_1262092251_state > $o ) > $o] :
      ( ( insert1042460334tate_o @ A_48 @ B_29 )
      = ( collec313158217tate_o
        @ ^ [X_1: hoare_1262092251_state > $o] :
            ( (|) @ ( X_1 = A_48 ) @ ( member907417095tate_o @ X_1 @ B_29 ) ) ) ) )).

thf(fact_190_insertI1,axiom,(
    ! [A_47: pname,B_28: pname > $o] :
      ( member_pname @ A_47 @ ( insert_pname @ A_47 @ B_28 ) ) )).

thf(fact_191_insertI1,axiom,(
    ! [A_47: hoare_1262092251_state,B_28: hoare_1262092251_state > $o] :
      ( member5164104_state @ A_47 @ ( insert81609953_state @ A_47 @ B_28 ) ) )).

thf(fact_192_equalityE,axiom,(
    ! [A_46: pname > $o,B_27: pname > $o] :
      ( ( A_46 = B_27 )
     => ~ ( ( ord_less_eq_pname_o @ A_46 @ B_27 )
         => ~ ( ord_less_eq_pname_o @ B_27 @ A_46 ) ) ) )).

thf(fact_193_equalityE,axiom,(
    ! [A_46: hoare_1262092251_state > $o,B_27: hoare_1262092251_state > $o] :
      ( ( A_46 = B_27 )
     => ~ ( ( ord_le870406270tate_o @ A_46 @ B_27 )
         => ~ ( ord_le870406270tate_o @ B_27 @ A_46 ) ) ) )).

thf(fact_194_subset__trans,axiom,(
    ! [C_4: pname > $o,A_45: pname > $o,B_26: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_45 @ B_26 )
     => ( ( ord_less_eq_pname_o @ B_26 @ C_4 )
       => ( ord_less_eq_pname_o @ A_45 @ C_4 ) ) ) )).

thf(fact_195_subset__trans,axiom,(
    ! [C_4: hoare_1262092251_state > $o,A_45: hoare_1262092251_state > $o,B_26: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_45 @ B_26 )
     => ( ( ord_le870406270tate_o @ B_26 @ C_4 )
       => ( ord_le870406270tate_o @ A_45 @ C_4 ) ) ) )).

thf(fact_196_set__mp,axiom,(
    ! [X_10: pname,A_44: pname > $o,B_25: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_44 @ B_25 )
     => ( ( member_pname @ X_10 @ A_44 )
       => ( member_pname @ X_10 @ B_25 ) ) ) )).

thf(fact_197_set__mp,axiom,(
    ! [X_10: hoare_1262092251_state,A_44: hoare_1262092251_state > $o,B_25: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_44 @ B_25 )
     => ( ( member5164104_state @ X_10 @ A_44 )
       => ( member5164104_state @ X_10 @ B_25 ) ) ) )).

thf(fact_198_set__rev__mp,axiom,(
    ! [B_24: pname > $o,X_9: pname,A_43: pname > $o] :
      ( ( member_pname @ X_9 @ A_43 )
     => ( ( ord_less_eq_pname_o @ A_43 @ B_24 )
       => ( member_pname @ X_9 @ B_24 ) ) ) )).

thf(fact_199_set__rev__mp,axiom,(
    ! [B_24: hoare_1262092251_state > $o,X_9: hoare_1262092251_state,A_43: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ X_9 @ A_43 )
     => ( ( ord_le870406270tate_o @ A_43 @ B_24 )
       => ( member5164104_state @ X_9 @ B_24 ) ) ) )).

thf(fact_200_in__mono,axiom,(
    ! [X_8: pname,A_42: pname > $o,B_23: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_42 @ B_23 )
     => ( ( member_pname @ X_8 @ A_42 )
       => ( member_pname @ X_8 @ B_23 ) ) ) )).

thf(fact_201_in__mono,axiom,(
    ! [X_8: hoare_1262092251_state,A_42: hoare_1262092251_state > $o,B_23: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_42 @ B_23 )
     => ( ( member5164104_state @ X_8 @ A_42 )
       => ( member5164104_state @ X_8 @ B_23 ) ) ) )).

thf(fact_202_equalityD2,axiom,(
    ! [A_41: pname > $o,B_22: pname > $o] :
      ( ( A_41 = B_22 )
     => ( ord_less_eq_pname_o @ B_22 @ A_41 ) ) )).

thf(fact_203_equalityD2,axiom,(
    ! [A_41: hoare_1262092251_state > $o,B_22: hoare_1262092251_state > $o] :
      ( ( A_41 = B_22 )
     => ( ord_le870406270tate_o @ B_22 @ A_41 ) ) )).

thf(fact_204_equalityD1,axiom,(
    ! [A_40: pname > $o,B_21: pname > $o] :
      ( ( A_40 = B_21 )
     => ( ord_less_eq_pname_o @ A_40 @ B_21 ) ) )).

thf(fact_205_equalityD1,axiom,(
    ! [A_40: hoare_1262092251_state > $o,B_21: hoare_1262092251_state > $o] :
      ( ( A_40 = B_21 )
     => ( ord_le870406270tate_o @ A_40 @ B_21 ) ) )).

thf(fact_206_set__eq__subset,axiom,(
    ! [A_39: pname > $o,B_20: pname > $o] :
      ( ( A_39 = B_20 )
    <=> ( ( ord_less_eq_pname_o @ A_39 @ B_20 )
        & ( ord_less_eq_pname_o @ B_20 @ A_39 ) ) ) )).

thf(fact_207_set__eq__subset,axiom,(
    ! [A_39: hoare_1262092251_state > $o,B_20: hoare_1262092251_state > $o] :
      ( ( A_39 = B_20 )
    <=> ( ( ord_le870406270tate_o @ A_39 @ B_20 )
        & ( ord_le870406270tate_o @ B_20 @ A_39 ) ) ) )).

thf(fact_208_subset__refl,axiom,(
    ! [A_38: pname > $o] :
      ( ord_less_eq_pname_o @ A_38 @ A_38 ) )).

thf(fact_209_subset__refl,axiom,(
    ! [A_38: hoare_1262092251_state > $o] :
      ( ord_le870406270tate_o @ A_38 @ A_38 ) )).

thf(fact_210_rev__image__eqI,axiom,(
    ! [B_19: hoare_1262092251_state,F_13: pname > hoare_1262092251_state,X_7: pname,A_37: pname > $o] :
      ( ( member_pname @ X_7 @ A_37 )
     => ( ( B_19
          = ( F_13 @ X_7 ) )
       => ( member5164104_state @ B_19 @ ( image_669833818_state @ F_13 @ A_37 ) ) ) ) )).

thf(fact_211_imageI,axiom,(
    ! [F_12: pname > hoare_1262092251_state,X_6: pname,A_36: pname > $o] :
      ( ( member_pname @ X_6 @ A_36 )
     => ( member5164104_state @ ( F_12 @ X_6 ) @ ( image_669833818_state @ F_12 @ A_36 ) ) ) )).

thf(fact_212_image__iff,axiom,(
    ! [Z: hoare_1262092251_state,F_11: pname > hoare_1262092251_state,A_35: pname > $o] :
      ( ( member5164104_state @ Z @ ( image_669833818_state @ F_11 @ A_35 ) )
    <=> ? [X_1: pname] :
          ( ( member_pname @ X_1 @ A_35 )
          & ( Z
            = ( F_11 @ X_1 ) ) ) ) )).

thf(fact_213_finite__Collect__disjI,axiom,(
    ! [P_5: pname > $o,Q: pname > $o] :
      ( ( finite_finite_pname
        @ ( collect_pname
          @ ^ [X_1: pname] :
              ( (|) @ ( P_5 @ X_1 ) @ ( Q @ X_1 ) ) ) )
    <=> ( ( finite_finite_pname @ ( collect_pname @ P_5 ) )
        & ( finite_finite_pname @ ( collect_pname @ Q ) ) ) ) )).

thf(fact_214_finite__Collect__disjI,axiom,(
    ! [P_5: hoare_1262092251_state > $o,Q: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state
        @ ( collec1121927558_state
          @ ^ [X_1: hoare_1262092251_state] :
              ( (|) @ ( P_5 @ X_1 ) @ ( Q @ X_1 ) ) ) )
    <=> ( ( finite1178804552_state @ ( collec1121927558_state @ P_5 ) )
        & ( finite1178804552_state @ ( collec1121927558_state @ Q ) ) ) ) )).

thf(fact_215_finite__Collect__disjI,axiom,(
    ! [P_5: ( pname > $o ) > $o,Q: ( pname > $o ) > $o] :
      ( ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [X_1: pname > $o] :
              ( (|) @ ( P_5 @ X_1 ) @ ( Q @ X_1 ) ) ) )
    <=> ( ( finite297249702name_o @ ( collect_pname_o @ P_5 ) )
        & ( finite297249702name_o @ ( collect_pname_o @ Q ) ) ) ) )).

thf(fact_216_finite__Collect__disjI,axiom,(
    ! [P_5: ( hoare_1262092251_state > $o ) > $o,Q: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o
        @ ( collec313158217tate_o
          @ ^ [X_1: hoare_1262092251_state > $o] :
              ( (|) @ ( P_5 @ X_1 ) @ ( Q @ X_1 ) ) ) )
    <=> ( ( finite1423311111tate_o @ ( collec313158217tate_o @ P_5 ) )
        & ( finite1423311111tate_o @ ( collec313158217tate_o @ Q ) ) ) ) )).

thf(fact_217_insert__compr__raw,axiom,(
    ! [X_1: pname,Xa: pname > $o] :
      ( ( insert_pname @ X_1 @ Xa )
      = ( collect_pname
        @ ^ [Y_1: pname] :
            ( (|) @ ( Y_1 = X_1 ) @ ( member_pname @ Y_1 @ Xa ) ) ) ) )).

thf(fact_218_insert__compr__raw,axiom,(
    ! [X_1: hoare_1262092251_state,Xa: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ X_1 @ Xa )
      = ( collec1121927558_state
        @ ^ [Y_1: hoare_1262092251_state] :
            ( (|) @ ( Y_1 = X_1 ) @ ( member5164104_state @ Y_1 @ Xa ) ) ) ) )).

thf(fact_219_insert__compr__raw,axiom,(
    ! [X_1: pname > $o,Xa: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ X_1 @ Xa )
      = ( collect_pname_o
        @ ^ [Y_1: pname > $o] :
            ( (|) @ ( Y_1 = X_1 ) @ ( member_pname_o @ Y_1 @ Xa ) ) ) ) )).

thf(fact_220_insert__compr__raw,axiom,(
    ! [X_1: hoare_1262092251_state > $o,Xa: ( hoare_1262092251_state > $o ) > $o] :
      ( ( insert1042460334tate_o @ X_1 @ Xa )
      = ( collec313158217tate_o
        @ ^ [Y_1: hoare_1262092251_state > $o] :
            ( (|) @ ( Y_1 = X_1 ) @ ( member907417095tate_o @ Y_1 @ Xa ) ) ) ) )).

thf(fact_221_singleton__inject,axiom,(
    ! [A_34: pname,B_18: pname] :
      ( ( ( insert_pname @ A_34 @ bot_bot_pname_o )
        = ( insert_pname @ B_18 @ bot_bot_pname_o ) )
     => ( A_34 = B_18 ) ) )).

thf(fact_222_singleton__inject,axiom,(
    ! [A_34: hoare_1262092251_state,B_18: hoare_1262092251_state] :
      ( ( ( insert81609953_state @ A_34 @ bot_bo113204042tate_o )
        = ( insert81609953_state @ B_18 @ bot_bo113204042tate_o ) )
     => ( A_34 = B_18 ) ) )).

thf(fact_223_singletonE,axiom,(
    ! [B_17: pname,A_33: pname] :
      ( ( member_pname @ B_17 @ ( insert_pname @ A_33 @ bot_bot_pname_o ) )
     => ( B_17 = A_33 ) ) )).

thf(fact_224_singletonE,axiom,(
    ! [B_17: hoare_1262092251_state,A_33: hoare_1262092251_state] :
      ( ( member5164104_state @ B_17 @ ( insert81609953_state @ A_33 @ bot_bo113204042tate_o ) )
     => ( B_17 = A_33 ) ) )).

thf(fact_225_doubleton__eq__iff,axiom,(
    ! [A_32: pname,B_16: pname,C_3: pname,D_1: pname] :
      ( ( ( insert_pname @ A_32 @ ( insert_pname @ B_16 @ bot_bot_pname_o ) )
        = ( insert_pname @ C_3 @ ( insert_pname @ D_1 @ bot_bot_pname_o ) ) )
    <=> ( ( ( A_32 = C_3 )
          & ( B_16 = D_1 ) )
        | ( ( A_32 = D_1 )
          & ( B_16 = C_3 ) ) ) ) )).

thf(fact_226_doubleton__eq__iff,axiom,(
    ! [A_32: hoare_1262092251_state,B_16: hoare_1262092251_state,C_3: hoare_1262092251_state,D_1: hoare_1262092251_state] :
      ( ( ( insert81609953_state @ A_32 @ ( insert81609953_state @ B_16 @ bot_bo113204042tate_o ) )
        = ( insert81609953_state @ C_3 @ ( insert81609953_state @ D_1 @ bot_bo113204042tate_o ) ) )
    <=> ( ( ( A_32 = C_3 )
          & ( B_16 = D_1 ) )
        | ( ( A_32 = D_1 )
          & ( B_16 = C_3 ) ) ) ) )).

thf(fact_227_singleton__iff,axiom,(
    ! [B_15: pname,A_31: pname] :
      ( ( member_pname @ B_15 @ ( insert_pname @ A_31 @ bot_bot_pname_o ) )
    <=> ( B_15 = A_31 ) ) )).

thf(fact_228_singleton__iff,axiom,(
    ! [B_15: hoare_1262092251_state,A_31: hoare_1262092251_state] :
      ( ( member5164104_state @ B_15 @ ( insert81609953_state @ A_31 @ bot_bo113204042tate_o ) )
    <=> ( B_15 = A_31 ) ) )).

thf(fact_229_insert__not__empty,axiom,(
    ! [A_30: pname,A_29: pname > $o] :
      ( ( insert_pname @ A_30 @ A_29 )
     != bot_bot_pname_o ) )).

thf(fact_230_insert__not__empty,axiom,(
    ! [A_30: hoare_1262092251_state,A_29: hoare_1262092251_state > $o] :
      ( ( insert81609953_state @ A_30 @ A_29 )
     != bot_bo113204042tate_o ) )).

thf(fact_231_empty__not__insert,axiom,(
    ! [A_28: pname,A_27: pname > $o] :
      ( bot_bot_pname_o
     != ( insert_pname @ A_28 @ A_27 ) ) )).

thf(fact_232_empty__not__insert,axiom,(
    ! [A_28: hoare_1262092251_state,A_27: hoare_1262092251_state > $o] :
      ( bot_bo113204042tate_o
     != ( insert81609953_state @ A_28 @ A_27 ) ) )).

thf(fact_233_finite__insert,axiom,(
    ! [A_26: pname,A_25: pname > $o] :
      ( ( finite_finite_pname @ ( insert_pname @ A_26 @ A_25 ) )
    <=> ( finite_finite_pname @ A_25 ) ) )).

thf(fact_234_finite__insert,axiom,(
    ! [A_26: hoare_1262092251_state,A_25: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ ( insert81609953_state @ A_26 @ A_25 ) )
    <=> ( finite1178804552_state @ A_25 ) ) )).

thf(fact_235_finite__insert,axiom,(
    ! [A_26: pname > $o,A_25: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ ( insert_pname_o @ A_26 @ A_25 ) )
    <=> ( finite297249702name_o @ A_25 ) ) )).

thf(fact_236_finite__insert,axiom,(
    ! [A_26: hoare_1262092251_state > $o,A_25: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ ( insert1042460334tate_o @ A_26 @ A_25 ) )
    <=> ( finite1423311111tate_o @ A_25 ) ) )).

thf(fact_237_subset__empty,axiom,(
    ! [A_24: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_24 @ bot_bot_pname_o )
    <=> ( A_24 = bot_bot_pname_o ) ) )).

thf(fact_238_subset__empty,axiom,(
    ! [A_24: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_24 @ bot_bo113204042tate_o )
    <=> ( A_24 = bot_bo113204042tate_o ) ) )).

thf(fact_239_image__is__empty,axiom,(
    ! [F_10: pname > hoare_1262092251_state,A_23: pname > $o] :
      ( ( ( image_669833818_state @ F_10 @ A_23 )
        = bot_bo113204042tate_o )
    <=> ( A_23 = bot_bot_pname_o ) ) )).

thf(fact_240_image__empty,axiom,(
    ! [F_9: pname > hoare_1262092251_state] :
      ( ( image_669833818_state @ F_9 @ bot_bot_pname_o )
      = bot_bo113204042tate_o ) )).

thf(fact_241_empty__is__image,axiom,(
    ! [F_8: pname > hoare_1262092251_state,A_22: pname > $o] :
      ( ( bot_bo113204042tate_o
        = ( image_669833818_state @ F_8 @ A_22 ) )
    <=> ( A_22 = bot_bot_pname_o ) ) )).

thf(fact_242_finite__subset,axiom,(
    ! [A_21: ( pname > $o ) > $o,B_14: ( pname > $o ) > $o] :
      ( ( ord_le1205211808me_o_o @ A_21 @ B_14 )
     => ( ( finite297249702name_o @ B_14 )
       => ( finite297249702name_o @ A_21 ) ) ) )).

thf(fact_243_finite__subset,axiom,(
    ! [A_21: ( hoare_1262092251_state > $o ) > $o,B_14: ( hoare_1262092251_state > $o ) > $o] :
      ( ( ord_le2012720639te_o_o @ A_21 @ B_14 )
     => ( ( finite1423311111tate_o @ B_14 )
       => ( finite1423311111tate_o @ A_21 ) ) ) )).

thf(fact_244_finite__subset,axiom,(
    ! [A_21: pname > $o,B_14: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_21 @ B_14 )
     => ( ( finite_finite_pname @ B_14 )
       => ( finite_finite_pname @ A_21 ) ) ) )).

thf(fact_245_finite__subset,axiom,(
    ! [A_21: hoare_1262092251_state > $o,B_14: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_21 @ B_14 )
     => ( ( finite1178804552_state @ B_14 )
       => ( finite1178804552_state @ A_21 ) ) ) )).

thf(fact_246_rev__finite__subset,axiom,(
    ! [A_20: ( pname > $o ) > $o,B_13: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ B_13 )
     => ( ( ord_le1205211808me_o_o @ A_20 @ B_13 )
       => ( finite297249702name_o @ A_20 ) ) ) )).

thf(fact_247_rev__finite__subset,axiom,(
    ! [A_20: ( hoare_1262092251_state > $o ) > $o,B_13: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ B_13 )
     => ( ( ord_le2012720639te_o_o @ A_20 @ B_13 )
       => ( finite1423311111tate_o @ A_20 ) ) ) )).

thf(fact_248_rev__finite__subset,axiom,(
    ! [A_20: pname > $o,B_13: pname > $o] :
      ( ( finite_finite_pname @ B_13 )
     => ( ( ord_less_eq_pname_o @ A_20 @ B_13 )
       => ( finite_finite_pname @ A_20 ) ) ) )).

thf(fact_249_rev__finite__subset,axiom,(
    ! [A_20: hoare_1262092251_state > $o,B_13: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ B_13 )
     => ( ( ord_le870406270tate_o @ A_20 @ B_13 )
       => ( finite1178804552_state @ A_20 ) ) ) )).

thf(fact_250_insert__mono,axiom,(
    ! [A_19: pname,C_2: pname > $o,D: pname > $o] :
      ( ( ord_less_eq_pname_o @ C_2 @ D )
     => ( ord_less_eq_pname_o @ ( insert_pname @ A_19 @ C_2 ) @ ( insert_pname @ A_19 @ D ) ) ) )).

thf(fact_251_insert__mono,axiom,(
    ! [A_19: hoare_1262092251_state,C_2: hoare_1262092251_state > $o,D: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ C_2 @ D )
     => ( ord_le870406270tate_o @ ( insert81609953_state @ A_19 @ C_2 ) @ ( insert81609953_state @ A_19 @ D ) ) ) )).

thf(fact_252_mem__def,axiom,(
    ! [X_5: pname,A_18: pname > $o] :
      ( ( member_pname @ X_5 @ A_18 )
    <=> ( A_18 @ X_5 ) ) )).

thf(fact_253_mem__def,axiom,(
    ! [X_5: hoare_1262092251_state,A_18: hoare_1262092251_state > $o] :
      ( ( member5164104_state @ X_5 @ A_18 )
    <=> ( A_18 @ X_5 ) ) )).

thf(fact_254_Collect__def,axiom,(
    ! [P_4: pname > $o] :
      ( ( collect_pname @ P_4 )
      = P_4 ) )).

thf(fact_255_Collect__def,axiom,(
    ! [P_4: hoare_1262092251_state > $o] :
      ( ( collec1121927558_state @ P_4 )
      = P_4 ) )).

thf(fact_256_Collect__def,axiom,(
    ! [P_4: ( pname > $o ) > $o] :
      ( ( collect_pname_o @ P_4 )
      = P_4 ) )).

thf(fact_257_Collect__def,axiom,(
    ! [P_4: ( hoare_1262092251_state > $o ) > $o] :
      ( ( collec313158217tate_o @ P_4 )
      = P_4 ) )).

thf(fact_258_subset__insertI2,axiom,(
    ! [B_12: pname,A_17: pname > $o,B_11: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_17 @ B_11 )
     => ( ord_less_eq_pname_o @ A_17 @ ( insert_pname @ B_12 @ B_11 ) ) ) )).

thf(fact_259_subset__insertI2,axiom,(
    ! [B_12: hoare_1262092251_state,A_17: hoare_1262092251_state > $o,B_11: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ A_17 @ B_11 )
     => ( ord_le870406270tate_o @ A_17 @ ( insert81609953_state @ B_12 @ B_11 ) ) ) )).

thf(fact_260_subset__insert,axiom,(
    ! [B_10: pname > $o,X_4: pname,A_16: pname > $o] :
      ( ~ ( member_pname @ X_4 @ A_16 )
     => ( ( ord_less_eq_pname_o @ A_16 @ ( insert_pname @ X_4 @ B_10 ) )
      <=> ( ord_less_eq_pname_o @ A_16 @ B_10 ) ) ) )).

thf(fact_261_subset__insert,axiom,(
    ! [B_10: hoare_1262092251_state > $o,X_4: hoare_1262092251_state,A_16: hoare_1262092251_state > $o] :
      ( ~ ( member5164104_state @ X_4 @ A_16 )
     => ( ( ord_le870406270tate_o @ A_16 @ ( insert81609953_state @ X_4 @ B_10 ) )
      <=> ( ord_le870406270tate_o @ A_16 @ B_10 ) ) ) )).

thf(fact_262_insert__subset,axiom,(
    ! [X_3: pname,A_15: pname > $o,B_9: pname > $o] :
      ( ( ord_less_eq_pname_o @ ( insert_pname @ X_3 @ A_15 ) @ B_9 )
    <=> ( ( member_pname @ X_3 @ B_9 )
        & ( ord_less_eq_pname_o @ A_15 @ B_9 ) ) ) )).

thf(fact_263_insert__subset,axiom,(
    ! [X_3: hoare_1262092251_state,A_15: hoare_1262092251_state > $o,B_9: hoare_1262092251_state > $o] :
      ( ( ord_le870406270tate_o @ ( insert81609953_state @ X_3 @ A_15 ) @ B_9 )
    <=> ( ( member5164104_state @ X_3 @ B_9 )
        & ( ord_le870406270tate_o @ A_15 @ B_9 ) ) ) )).

thf(fact_264_subset__insertI,axiom,(
    ! [B_8: pname > $o,A_14: pname] :
      ( ord_less_eq_pname_o @ B_8 @ ( insert_pname @ A_14 @ B_8 ) ) )).

thf(fact_265_subset__insertI,axiom,(
    ! [B_8: hoare_1262092251_state > $o,A_14: hoare_1262092251_state] :
      ( ord_le870406270tate_o @ B_8 @ ( insert81609953_state @ A_14 @ B_8 ) ) )).

thf(fact_266_insert__image,axiom,(
    ! [F_7: pname > hoare_1262092251_state,X_2: pname,A_13: pname > $o] :
      ( ( member_pname @ X_2 @ A_13 )
     => ( ( insert81609953_state @ ( F_7 @ X_2 ) @ ( image_669833818_state @ F_7 @ A_13 ) )
        = ( image_669833818_state @ F_7 @ A_13 ) ) ) )).

thf(fact_267_image__insert,axiom,(
    ! [F_6: pname > hoare_1262092251_state,A_12: pname,B_7: pname > $o] :
      ( ( image_669833818_state @ F_6 @ ( insert_pname @ A_12 @ B_7 ) )
      = ( insert81609953_state @ ( F_6 @ A_12 ) @ ( image_669833818_state @ F_6 @ B_7 ) ) ) )).

thf(fact_268_image__mono,axiom,(
    ! [F_5: pname > hoare_1262092251_state,A_11: pname > $o,B_6: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_11 @ B_6 )
     => ( ord_le870406270tate_o @ ( image_669833818_state @ F_5 @ A_11 ) @ ( image_669833818_state @ F_5 @ B_6 ) ) ) )).

thf(fact_269_subset__image__iff,axiom,(
    ! [B_5: hoare_1262092251_state > $o,F_4: pname > hoare_1262092251_state,A_10: pname > $o] :
      ( ( ord_le870406270tate_o @ B_5 @ ( image_669833818_state @ F_4 @ A_10 ) )
    <=> ? [AA: pname > $o] :
          ( ( ord_less_eq_pname_o @ AA @ A_10 )
          & ( B_5
            = ( image_669833818_state @ F_4 @ AA ) ) ) ) )).

thf(fact_270_domI,axiom,(
    ! [M: pname > option_com,A_9: pname,B_4: com] :
      ( ( ( M @ A_9 )
        = ( some_com @ B_4 ) )
     => ( member_pname @ A_9 @ ( dom_pname_com @ M ) ) ) )).

thf(fact_271_Collect__conv__if,axiom,(
    ! [P_3: pname > $o,A_8: pname] :
      ( ( ( P_3 @ A_8 )
       => ( ( collect_pname
            @ ^ [X_1: pname] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = ( insert_pname @ A_8 @ bot_bot_pname_o ) ) )
      & ( ~ ( P_3 @ A_8 )
       => ( ( collect_pname
            @ ^ [X_1: pname] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = bot_bot_pname_o ) ) ) )).

thf(fact_272_Collect__conv__if,axiom,(
    ! [P_3: hoare_1262092251_state > $o,A_8: hoare_1262092251_state] :
      ( ( ( P_3 @ A_8 )
       => ( ( collec1121927558_state
            @ ^ [X_1: hoare_1262092251_state] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = ( insert81609953_state @ A_8 @ bot_bo113204042tate_o ) ) )
      & ( ~ ( P_3 @ A_8 )
       => ( ( collec1121927558_state
            @ ^ [X_1: hoare_1262092251_state] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = bot_bo113204042tate_o ) ) ) )).

thf(fact_273_Collect__conv__if,axiom,(
    ! [P_3: ( pname > $o ) > $o,A_8: pname > $o] :
      ( ( ( P_3 @ A_8 )
       => ( ( collect_pname_o
            @ ^ [X_1: pname > $o] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = ( insert_pname_o @ A_8 @ bot_bot_pname_o_o ) ) )
      & ( ~ ( P_3 @ A_8 )
       => ( ( collect_pname_o
            @ ^ [X_1: pname > $o] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = bot_bot_pname_o_o ) ) ) )).

thf(fact_274_Collect__conv__if,axiom,(
    ! [P_3: ( hoare_1262092251_state > $o ) > $o,A_8: hoare_1262092251_state > $o] :
      ( ( ( P_3 @ A_8 )
       => ( ( collec313158217tate_o
            @ ^ [X_1: hoare_1262092251_state > $o] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = ( insert1042460334tate_o @ A_8 @ bot_bo1962689075te_o_o ) ) )
      & ( ~ ( P_3 @ A_8 )
       => ( ( collec313158217tate_o
            @ ^ [X_1: hoare_1262092251_state > $o] :
                ( (&) @ ( X_1 = A_8 ) @ ( P_3 @ X_1 ) ) )
          = bot_bo1962689075te_o_o ) ) ) )).

thf(fact_275_Collect__conv__if2,axiom,(
    ! [P_2: pname > $o,A_7: pname] :
      ( ( ( P_2 @ A_7 )
       => ( ( collect_pname
            @ ^ [X_1: pname] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = ( insert_pname @ A_7 @ bot_bot_pname_o ) ) )
      & ( ~ ( P_2 @ A_7 )
       => ( ( collect_pname
            @ ^ [X_1: pname] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = bot_bot_pname_o ) ) ) )).

thf(fact_276_Collect__conv__if2,axiom,(
    ! [P_2: hoare_1262092251_state > $o,A_7: hoare_1262092251_state] :
      ( ( ( P_2 @ A_7 )
       => ( ( collec1121927558_state
            @ ^ [X_1: hoare_1262092251_state] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = ( insert81609953_state @ A_7 @ bot_bo113204042tate_o ) ) )
      & ( ~ ( P_2 @ A_7 )
       => ( ( collec1121927558_state
            @ ^ [X_1: hoare_1262092251_state] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = bot_bo113204042tate_o ) ) ) )).

thf(fact_277_Collect__conv__if2,axiom,(
    ! [P_2: ( pname > $o ) > $o,A_7: pname > $o] :
      ( ( ( P_2 @ A_7 )
       => ( ( collect_pname_o
            @ ^ [X_1: pname > $o] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = ( insert_pname_o @ A_7 @ bot_bot_pname_o_o ) ) )
      & ( ~ ( P_2 @ A_7 )
       => ( ( collect_pname_o
            @ ^ [X_1: pname > $o] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = bot_bot_pname_o_o ) ) ) )).

thf(fact_278_Collect__conv__if2,axiom,(
    ! [P_2: ( hoare_1262092251_state > $o ) > $o,A_7: hoare_1262092251_state > $o] :
      ( ( ( P_2 @ A_7 )
       => ( ( collec313158217tate_o
            @ ^ [X_1: hoare_1262092251_state > $o] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = ( insert1042460334tate_o @ A_7 @ bot_bo1962689075te_o_o ) ) )
      & ( ~ ( P_2 @ A_7 )
       => ( ( collec313158217tate_o
            @ ^ [X_1: hoare_1262092251_state > $o] :
                ( (&) @ ( A_7 = X_1 ) @ ( P_2 @ X_1 ) ) )
          = bot_bo1962689075te_o_o ) ) ) )).

thf(fact_279_singleton__conv,axiom,(
    ! [A_6: pname] :
      ( ( collect_pname
        @ ^ [X_1: pname] : ( X_1 = A_6 ) )
      = ( insert_pname @ A_6 @ bot_bot_pname_o ) ) )).

thf(fact_280_singleton__conv,axiom,(
    ! [A_6: hoare_1262092251_state] :
      ( ( collec1121927558_state
        @ ^ [X_1: hoare_1262092251_state] : ( X_1 = A_6 ) )
      = ( insert81609953_state @ A_6 @ bot_bo113204042tate_o ) ) )).

thf(fact_281_singleton__conv,axiom,(
    ! [A_6: pname > $o] :
      ( ( collect_pname_o
        @ ^ [X_1: pname > $o] : ( X_1 = A_6 ) )
      = ( insert_pname_o @ A_6 @ bot_bot_pname_o_o ) ) )).

thf(fact_282_singleton__conv,axiom,(
    ! [A_6: hoare_1262092251_state > $o] :
      ( ( collec313158217tate_o
        @ ^ [X_1: hoare_1262092251_state > $o] : ( X_1 = A_6 ) )
      = ( insert1042460334tate_o @ A_6 @ bot_bo1962689075te_o_o ) ) )).

thf(fact_283_singleton__conv2,axiom,(
    ! [A_5: pname] :
      ( ( collect_pname @ ( fequal_pname @ A_5 ) )
      = ( insert_pname @ A_5 @ bot_bot_pname_o ) ) )).

thf(fact_284_singleton__conv2,axiom,(
    ! [A_5: hoare_1262092251_state] :
      ( ( collec1121927558_state @ ( fequal1925511196_state @ A_5 ) )
      = ( insert81609953_state @ A_5 @ bot_bo113204042tate_o ) ) )).

thf(fact_285_singleton__conv2,axiom,(
    ! [A_5: pname > $o] :
      ( ( collect_pname_o @ ( fequal_pname_o @ A_5 ) )
      = ( insert_pname_o @ A_5 @ bot_bot_pname_o_o ) ) )).

thf(fact_286_singleton__conv2,axiom,(
    ! [A_5: hoare_1262092251_state > $o] :
      ( ( collec313158217tate_o @ ( fequal1529404211tate_o @ A_5 ) )
      = ( insert1042460334tate_o @ A_5 @ bot_bo1962689075te_o_o ) ) )).

thf(fact_287_MGF__lemma1,axiom,(
    ! [C_1: com,G: hoare_1262092251_state > $o] :
      ( hoare_1821564147gleton
     => ( ! [X_1: pname] :
            ( ( member_pname @ X_1 @ ( dom_pname_com @ body ) )
           => ( hoare_930741239_state @ G @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ ( body_1 @ X_1 ) ) @ bot_bo113204042tate_o ) ) )
       => ( ( wt @ C_1 )
         => ( hoare_930741239_state @ G @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ C_1 ) @ bot_bo113204042tate_o ) ) ) ) ) )).

thf(fact_288_WT__bodiesD,axiom,(
    ! [Pn_1: pname,B_3: com] :
      ( wT_bodies
     => ( ( ( body @ Pn_1 )
          = ( some_com @ B_3 ) )
       => ( wt @ B_3 ) ) ) )).

thf(fact_289_imageE,axiom,(
    ! [B_2: hoare_1262092251_state,F_3: pname > hoare_1262092251_state,A_4: pname > $o] :
      ( ( member5164104_state @ B_2 @ ( image_669833818_state @ F_3 @ A_4 ) )
     => ~ ! [X_1: pname] :
            ( ( B_2
              = ( F_3 @ X_1 ) )
           => ~ ( member_pname @ X_1 @ A_4 ) ) ) )).

thf(fact_290_finite__subset__induct,axiom,(
    ! [P_1: ( pname > $o ) > $o,A_2: pname > $o,F_1: pname > $o] :
      ( ( finite_finite_pname @ F_1 )
     => ( ( ord_less_eq_pname_o @ F_1 @ A_2 )
       => ( ( P_1 @ bot_bot_pname_o )
         => ( ! [A_3: pname,F_2: pname > $o] :
                ( ( finite_finite_pname @ F_2 )
               => ( ( member_pname @ A_3 @ A_2 )
                 => ( ~ ( member_pname @ A_3 @ F_2 )
                   => ( ( P_1 @ F_2 )
                     => ( P_1 @ ( insert_pname @ A_3 @ F_2 ) ) ) ) ) )
           => ( P_1 @ F_1 ) ) ) ) ) )).

thf(fact_291_finite__subset__induct,axiom,(
    ! [P_1: ( hoare_1262092251_state > $o ) > $o,A_2: hoare_1262092251_state > $o,F_1: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ F_1 )
     => ( ( ord_le870406270tate_o @ F_1 @ A_2 )
       => ( ( P_1 @ bot_bo113204042tate_o )
         => ( ! [A_3: hoare_1262092251_state,F_2: hoare_1262092251_state > $o] :
                ( ( finite1178804552_state @ F_2 )
               => ( ( member5164104_state @ A_3 @ A_2 )
                 => ( ~ ( member5164104_state @ A_3 @ F_2 )
                   => ( ( P_1 @ F_2 )
                     => ( P_1 @ ( insert81609953_state @ A_3 @ F_2 ) ) ) ) ) )
           => ( P_1 @ F_1 ) ) ) ) ) )).

thf(fact_292_finite__subset__induct,axiom,(
    ! [P_1: ( ( pname > $o ) > $o ) > $o,A_2: ( pname > $o ) > $o,F_1: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_1 )
     => ( ( ord_le1205211808me_o_o @ F_1 @ A_2 )
       => ( ( P_1 @ bot_bot_pname_o_o )
         => ( ! [A_3: pname > $o,F_2: ( pname > $o ) > $o] :
                ( ( finite297249702name_o @ F_2 )
               => ( ( member_pname_o @ A_3 @ A_2 )
                 => ( ~ ( member_pname_o @ A_3 @ F_2 )
                   => ( ( P_1 @ F_2 )
                     => ( P_1 @ ( insert_pname_o @ A_3 @ F_2 ) ) ) ) ) )
           => ( P_1 @ F_1 ) ) ) ) ) )).

thf(fact_293_finite__subset__induct,axiom,(
    ! [P_1: ( ( hoare_1262092251_state > $o ) > $o ) > $o,A_2: ( hoare_1262092251_state > $o ) > $o,F_1: ( hoare_1262092251_state > $o ) > $o] :
      ( ( finite1423311111tate_o @ F_1 )
     => ( ( ord_le2012720639te_o_o @ F_1 @ A_2 )
       => ( ( P_1 @ bot_bo1962689075te_o_o )
         => ( ! [A_3: hoare_1262092251_state > $o,F_2: ( hoare_1262092251_state > $o ) > $o] :
                ( ( finite1423311111tate_o @ F_2 )
               => ( ( member907417095tate_o @ A_3 @ A_2 )
                 => ( ~ ( member907417095tate_o @ A_3 @ F_2 )
                   => ( ( P_1 @ F_2 )
                     => ( P_1 @ ( insert1042460334tate_o @ A_3 @ F_2 ) ) ) ) ) )
           => ( P_1 @ F_1 ) ) ) ) ) )).

thf(fact_294_WTs__elim__cases_I7_J,axiom,(
    ! [P: pname] :
      ( ( wt @ ( body_1 @ P ) )
     => ~ ! [Y_1: com] :
            ( ( body @ P )
           != ( some_com @ Y_1 ) ) ) )).

thf(fact_295_subsetI,axiom,(
    ! [B_1: pname > $o,A_1: pname > $o] :
      ( ! [X_1: pname] :
          ( ( member_pname @ X_1 @ A_1 )
         => ( member_pname @ X_1 @ B_1 ) )
     => ( ord_less_eq_pname_o @ A_1 @ B_1 ) ) )).

thf(fact_296_subsetI,axiom,(
    ! [B_1: hoare_1262092251_state > $o,A_1: hoare_1262092251_state > $o] :
      ( ! [X_1: hoare_1262092251_state] :
          ( ( member5164104_state @ X_1 @ A_1 )
         => ( member5164104_state @ X_1 @ B_1 ) )
     => ( ord_le870406270tate_o @ A_1 @ B_1 ) ) )).

thf(fact_297_finite__subset__image,axiom,(
    ! [F: pname > hoare_1262092251_state,A: pname > $o,B: hoare_1262092251_state > $o] :
      ( ( finite1178804552_state @ B )
     => ( ( ord_le870406270tate_o @ B @ ( image_669833818_state @ F @ A ) )
       => ? [C: pname > $o] :
            ( ( ord_less_eq_pname_o @ C @ A )
            & ( finite_finite_pname @ C )
            & ( B
              = ( image_669833818_state @ F @ C ) ) ) ) ) )).

thf(fact_298_finite__dom__body,axiom,
    ( finite_finite_pname @ ( dom_pname_com @ body ) )).

thf(fact_299_com_Osimps_I6_J,axiom,(
    ! [Pname_1: pname,Pname: pname] :
      ( ( ( body_1 @ Pname_1 )
        = ( body_1 @ Pname ) )
    <=> ( Pname_1 = Pname ) ) )).

%----Helper facts (8)
thf(help_fequal_1_1_fequal_000tc__Com__Opname_T,axiom,(
    ! [X: pname,Y: pname] :
      ( ~ ( fequal_pname @ X @ Y )
      | ( X = Y ) ) )).

thf(help_fequal_2_1_fequal_000tc__Com__Opname_T,axiom,(
    ! [X: pname,Y: pname] :
      ( ( X != Y )
      | ( fequal_pname @ X @ Y ) ) )).

thf(help_fequal_1_1_fequal_000_062_Itc__Com__Opname_M_Eo_J_T,axiom,(
    ! [X: pname > $o,Y: pname > $o] :
      ( ~ ( fequal_pname_o @ X @ Y )
      | ( X = Y ) ) )).

thf(help_fequal_2_1_fequal_000_062_Itc__Com__Opname_M_Eo_J_T,axiom,(
    ! [X: pname > $o,Y: pname > $o] :
      ( ( X != Y )
      | ( fequal_pname_o @ X @ Y ) ) )).

thf(help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com,axiom,(
    ! [X: hoare_1262092251_state,Y: hoare_1262092251_state] :
      ( ~ ( fequal1925511196_state @ X @ Y )
      | ( X = Y ) ) )).

thf(help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_Itc__Com,axiom,(
    ! [X: hoare_1262092251_state,Y: hoare_1262092251_state] :
      ( ( X != Y )
      | ( fequal1925511196_state @ X @ Y ) ) )).

thf(help_fequal_1_1_fequal_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It,axiom,(
    ! [X: hoare_1262092251_state > $o,Y: hoare_1262092251_state > $o] :
      ( ~ ( fequal1529404211tate_o @ X @ Y )
      | ( X = Y ) ) )).

thf(help_fequal_2_1_fequal_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It,axiom,(
    ! [X: hoare_1262092251_state > $o,Y: hoare_1262092251_state > $o] :
      ( ( X != Y )
      | ( fequal1529404211tate_o @ X @ Y ) ) )).

%----Conjectures (8)
thf(conj_0,hypothesis,(
    hoare_1821564147gleton )).

thf(conj_1,hypothesis,(
    wT_bodies )).

thf(conj_2,hypothesis,
    ( finite1178804552_state @ fa )).

thf(conj_3,hypothesis,(
    ~ ( member5164104_state @ ( hoare_Mirabelle_MGT @ y ) @ fa ) )).

thf(conj_4,hypothesis,
    ( ord_le870406270tate_o @ fa
    @ ( image_669833818_state
      @ ^ [Pn: pname] :
          ( hoare_Mirabelle_MGT @ ( the_com @ ( body @ Pn ) ) )
      @ ( dom_pname_com @ body ) ) )).

thf(conj_5,hypothesis,
    ( ( body @ pn )
    = ( some_com @ y ) )).

thf(conj_6,hypothesis,
    ( hoare_930741239_state
    @ ( image_669833818_state
      @ ^ [Pn: pname] :
          ( hoare_Mirabelle_MGT @ ( body_1 @ Pn ) )
      @ ( dom_pname_com @ body ) )
    @ fa )).

thf(conj_7,conjecture,
    ( hoare_930741239_state
    @ ( image_669833818_state
      @ ^ [Pn: pname] :
          ( hoare_Mirabelle_MGT @ ( body_1 @ Pn ) )
      @ ( dom_pname_com @ body ) )
    @ ( insert81609953_state @ ( hoare_Mirabelle_MGT @ y ) @ bot_bo113204042tate_o ) )).

%------------------------------------------------------------------------------