diff options
Diffstat (limited to 'test/regress/regress1/ho/NUM925^1.p')
| -rw-r--r-- | test/regress/regress1/ho/NUM925^1.p | 638 |
1 files changed, 638 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p new file mode 100644 index 000000000..d2977ddb8 --- /dev/null +++ b/test/regress/regress1/ho/NUM925^1.p @@ -0,0 +1,638 @@ +% COMMAND-LINE: --uf-ho +% EXPECT: % SZS status Theorem for NUM925^1 + +%------------------------------------------------------------------------------ +% File : NUM925^1 : TPTP v7.2.0. Released v5.3.0. +% Domain : Number Theory +% Problem : Sum of two squares line 192, 100 axioms selected +% Version : Especial. +% English : + +% Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day +% : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe +% Source : [Bla11] +% Names : s2s_100_thf_l192 [Bla11] + +% Status : Theorem +% Rating : 0.22 v7.2.0, 0.12 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.40 v5.3.0 +% Syntax : Number of formulae : 128 ( 0 unit; 21 type; 0 defn) +% Number of atoms : 868 ( 105 equality; 251 variable) +% Maximal formula depth : 11 ( 5 average) +% Number of connectives : 571 ( 20 ~; 4 |; 7 &; 495 @) +% ( 36 <=>; 9 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 18 ( 18 >; 0 *; 0 +; 0 <<) +% Number of symbols : 23 ( 21 :; 0 =) +% Number of variables : 118 ( 0 sgn; 118 !; 0 ?; 0 ^) +% ( 118 :; 0 !>; 0 ?*) +% ( 0 @-; 0 @+) +% SPC : TH0_THM_EQU_NAR + +% Comments : This file was generated by Isabelle (most likely Sledgehammer) +% 2011-08-09 19:10:38 +%------------------------------------------------------------------------------ +%----Should-be-implicit typings (2) +thf(ty_ty_tc__Int__Oint,type,( + int: $tType )). + +thf(ty_ty_tc__Nat__Onat,type,( + nat: $tType )). + +%----Explicit typings (19) +thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,( + one_one_int: int )). + +thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,( + one_one_nat: nat )). + +thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,( + plus_plus_int: int > int > int )). + +thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,( + plus_plus_nat: nat > nat > nat )). + +thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,( + zero_zero_int: int )). + +thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,( + zero_zero_nat: nat )). + +thf(sy_c_Int_OBit0,type,( + bit0: int > int )). + +thf(sy_c_Int_OBit1,type,( + bit1: int > int )). + +thf(sy_c_Int_OPls,type,( + pls: int )). + +thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,( + number_number_of_int: int > int )). + +thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,( + number_number_of_nat: int > nat )). + +thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Int__Oint,type,( + semiri1621563631at_int: nat > int )). + +thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Nat__Onat,type,( + semiri984289939at_nat: nat > nat )). + +thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,( + ord_less_int: int > int > $o )). + +thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,( + ord_less_nat: nat > nat > $o )). + +thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,( + power_power_int: int > nat > int )). + +thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,( + power_power_nat: nat > nat > nat )). + +thf(sy_v_n____,type,( + n: nat )). + +thf(sy_v_t____,type,( + t: int )). + +%----Relevant facts (106) +thf(fact_0_n1pos,axiom, + ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) )). + +thf(fact_1_t1,axiom, + ( ord_less_int @ one_one_int @ t )). + +thf(fact_2_sum__power2__eq__zero__iff,axiom,( + ! [X_3: int,Y_3: int] : + ( ( ( plus_plus_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) + = zero_zero_int ) + <=> ( ( X_3 = zero_zero_int ) + & ( Y_3 = zero_zero_int ) ) ) )). + +thf(fact_3_one__power2,axiom, + ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = one_one_int )). + +thf(fact_4_one__power2,axiom, + ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = one_one_nat )). + +thf(fact_5_zero__power2,axiom, + ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_int )). + +thf(fact_6_zero__power2,axiom, + ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_nat )). + +thf(fact_7_zero__eq__power2,axiom,( + ! [A_7: int] : + ( ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_int ) + <=> ( A_7 = zero_zero_int ) ) )). + +thf(fact_8_add__special_I2_J,axiom,( + ! [W_7: int] : + ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) ) + = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) )). + +thf(fact_9_add__special_I3_J,axiom,( + ! [V_5: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_5 ) @ one_one_int ) + = ( number_number_of_int @ ( plus_plus_int @ V_5 @ ( bit1 @ pls ) ) ) ) )). + +thf(fact_10_one__add__one__is__two,axiom, + ( ( plus_plus_int @ one_one_int @ one_one_int ) + = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_11_semiring__one__add__one__is__two,axiom, + ( ( plus_plus_int @ one_one_int @ one_one_int ) + = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_12_semiring__one__add__one__is__two,axiom, + ( ( plus_plus_nat @ one_one_nat @ one_one_nat ) + = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_13_quartic__square__square,axiom,( + ! [X_3: int] : + ( ( power_power_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) )). + +thf(fact_14_power__0__left__number__of,axiom,( + ! [W_6: int] : + ( ( ( ( number_number_of_nat @ W_6 ) + = zero_zero_nat ) + => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) ) + = one_one_int ) ) + & ( ( ( number_number_of_nat @ W_6 ) + != zero_zero_nat ) + => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) ) + = zero_zero_int ) ) ) )). + +thf(fact_15_power__0__left__number__of,axiom,( + ! [W_6: int] : + ( ( ( ( number_number_of_nat @ W_6 ) + = zero_zero_nat ) + => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) ) + = one_one_nat ) ) + & ( ( ( number_number_of_nat @ W_6 ) + != zero_zero_nat ) + => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) ) + = zero_zero_nat ) ) ) )). + +thf(fact_16_semiring__norm_I110_J,axiom, + ( one_one_int + = ( number_number_of_int @ ( bit1 @ pls ) ) )). + +thf(fact_17_numeral__1__eq__1,axiom, + ( ( number_number_of_int @ ( bit1 @ pls ) ) + = one_one_int )). + +thf(fact_18_n0,axiom, + ( ord_less_nat @ zero_zero_nat @ n )). + +thf(fact_19_zless__linear,axiom,( + ! [X_3: int,Y_3: int] : + ( ( ord_less_int @ X_3 @ Y_3 ) + | ( X_3 = Y_3 ) + | ( ord_less_int @ Y_3 @ X_3 ) ) )). + +thf(fact_20_less__number__of__int__code,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_21_plus__numeral__code_I9_J,axiom,( + ! [V_3: int,W_4: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ ( number_number_of_int @ W_4 ) ) + = ( number_number_of_int @ ( plus_plus_int @ V_3 @ W_4 ) ) ) )). + +thf(fact_22_less__number__of,axiom,( + ! [X_6: int,Y_5: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_5 ) ) + <=> ( ord_less_int @ X_6 @ Y_5 ) ) )). + +thf(fact_23_zero__is__num__zero,axiom, + ( zero_zero_int + = ( number_number_of_int @ pls ) )). + +thf(fact_24_zpower__int,axiom,( + ! [M: nat,N_1: nat] : + ( ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) + = ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) ) )). + +thf(fact_25_int__power,axiom,( + ! [M: nat,N_1: nat] : + ( ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) + = ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) ) )). + +thf(fact_26_zadd__int__left,axiom,( + ! [M: nat,N_1: nat,Z: int] : + ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( plus_plus_int @ ( semiri1621563631at_int @ N_1 ) @ Z ) ) + = ( plus_plus_int @ ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) @ Z ) ) )). + +thf(fact_27_zadd__int,axiom,( + ! [M: nat,N_1: nat] : + ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( semiri1621563631at_int @ N_1 ) ) + = ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) ) )). + +thf(fact_28_int__1,axiom, + ( ( semiri1621563631at_int @ one_one_nat ) + = one_one_int )). + +thf(fact_29_nat__number__of__Pls,axiom, + ( ( number_number_of_nat @ pls ) + = zero_zero_nat )). + +thf(fact_30_semiring__norm_I113_J,axiom, + ( zero_zero_nat + = ( number_number_of_nat @ pls ) )). + +thf(fact_31_int__eq__0__conv,axiom,( + ! [N_1: nat] : + ( ( ( semiri1621563631at_int @ N_1 ) + = zero_zero_int ) + <=> ( N_1 = zero_zero_nat ) ) )). + +thf(fact_32_int__0,axiom, + ( ( semiri1621563631at_int @ zero_zero_nat ) + = zero_zero_int )). + +thf(fact_33_nat__1__add__1,axiom, + ( ( plus_plus_nat @ one_one_nat @ one_one_nat ) + = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_34_less__int__code_I16_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_35_rel__simps_I17_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_36_rel__simps_I2_J,axiom,( + ~ ( ord_less_int @ pls @ pls ) )). + +thf(fact_37_less__int__code_I13_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_38_rel__simps_I14_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_39_zadd__strict__right__mono,axiom,( + ! [K: int,I: int,J: int] : + ( ( ord_less_int @ I @ J ) + => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) )). + +thf(fact_40_add__nat__number__of,axiom,( + ! [V_4: int,V_3: int] : + ( ( ( ord_less_int @ V_3 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ V_4 ) ) ) + & ( ~ ( ord_less_int @ V_3 @ pls ) + => ( ( ( ord_less_int @ V_4 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ V_3 ) ) ) + & ( ~ ( ord_less_int @ V_4 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ ( plus_plus_int @ V_3 @ V_4 ) ) ) ) ) ) ) )). + +thf(fact_41_one__is__num__one,axiom, + ( one_one_int + = ( number_number_of_int @ ( bit1 @ pls ) ) )). + +thf(fact_42_nat__numeral__1__eq__1,axiom, + ( ( number_number_of_nat @ ( bit1 @ pls ) ) + = one_one_nat )). + +thf(fact_43_Numeral1__eq1__nat,axiom, + ( one_one_nat + = ( number_number_of_nat @ ( bit1 @ pls ) ) )). + +thf(fact_44_eq__number__of,axiom,( + ! [X_5: int,Y_4: int] : + ( ( ( number_number_of_int @ X_5 ) + = ( number_number_of_int @ Y_4 ) ) + <=> ( X_5 = Y_4 ) ) )). + +thf(fact_45_number__of__reorient,axiom,( + ! [W_5: int,X_4: nat] : + ( ( ( number_number_of_nat @ W_5 ) + = X_4 ) + <=> ( X_4 + = ( number_number_of_nat @ W_5 ) ) ) )). + +thf(fact_46_number__of__reorient,axiom,( + ! [W_5: int,X_4: int] : + ( ( ( number_number_of_int @ W_5 ) + = X_4 ) + <=> ( X_4 + = ( number_number_of_int @ W_5 ) ) ) )). + +thf(fact_47_rel__simps_I51_J,axiom,( + ! [K: int,L: int] : + ( ( ( bit1 @ K ) + = ( bit1 @ L ) ) + <=> ( K = L ) ) )). + +thf(fact_48_rel__simps_I48_J,axiom,( + ! [K: int,L: int] : + ( ( ( bit0 @ K ) + = ( bit0 @ L ) ) + <=> ( K = L ) ) )). + +thf(fact_49_even__less__0__iff,axiom,( + ! [A_6: int] : + ( ( ord_less_int @ ( plus_plus_int @ A_6 @ A_6 ) @ zero_zero_int ) + <=> ( ord_less_int @ A_6 @ zero_zero_int ) ) )). + +thf(fact_50_zadd__assoc,axiom,( + ! [Z1: int,Z2: int,Z3: int] : + ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 ) + = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) )). + +thf(fact_51_zadd__left__commute,axiom,( + ! [X_3: int,Y_3: int,Z: int] : + ( ( plus_plus_int @ X_3 @ ( plus_plus_int @ Y_3 @ Z ) ) + = ( plus_plus_int @ Y_3 @ ( plus_plus_int @ X_3 @ Z ) ) ) )). + +thf(fact_52_zadd__commute,axiom,( + ! [Z: int,W_4: int] : + ( ( plus_plus_int @ Z @ W_4 ) + = ( plus_plus_int @ W_4 @ Z ) ) )). + +thf(fact_53_int__int__eq,axiom,( + ! [M: nat,N_1: nat] : + ( ( ( semiri1621563631at_int @ M ) + = ( semiri1621563631at_int @ N_1 ) ) + <=> ( M = N_1 ) ) )). + +thf(fact_54_less__special_I3_J,axiom,( + ! [X_2: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_2 ) @ zero_zero_int ) + <=> ( ord_less_int @ X_2 @ pls ) ) )). + +thf(fact_55_less__special_I1_J,axiom,( + ! [Y_2: int] : + ( ( ord_less_int @ zero_zero_int @ ( number_number_of_int @ Y_2 ) ) + <=> ( ord_less_int @ pls @ Y_2 ) ) )). + +thf(fact_56_rel__simps_I12_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ pls ) + <=> ( ord_less_int @ K @ pls ) ) )). + +thf(fact_57_less__int__code_I15_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_58_rel__simps_I16_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_59_rel__simps_I10_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ ( bit0 @ K ) @ pls ) + <=> ( ord_less_int @ K @ pls ) ) )). + +thf(fact_60_rel__simps_I4_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ pls @ ( bit0 @ K ) ) + <=> ( ord_less_int @ pls @ K ) ) )). + +thf(fact_61_bin__less__0__simps_I4_J,axiom,( + ! [W_4: int] : + ( ( ord_less_int @ ( bit1 @ W_4 ) @ zero_zero_int ) + <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) )). + +thf(fact_62_bin__less__0__simps_I1_J,axiom,( + ~ ( ord_less_int @ pls @ zero_zero_int ) )). + +thf(fact_63_bin__less__0__simps_I3_J,axiom,( + ! [W_4: int] : + ( ( ord_less_int @ ( bit0 @ W_4 ) @ zero_zero_int ) + <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) )). + +thf(fact_64_int__0__less__1,axiom, + ( ord_less_int @ zero_zero_int @ one_one_int )). + +thf(fact_65_zless__add1__eq,axiom,( + ! [W_4: int,Z: int] : + ( ( ord_less_int @ W_4 @ ( plus_plus_int @ Z @ one_one_int ) ) + <=> ( ( ord_less_int @ W_4 @ Z ) + | ( W_4 = Z ) ) ) )). + +thf(fact_66_int__less__0__conv,axiom,( + ! [K: nat] : + ~ ( ord_less_int @ ( semiri1621563631at_int @ K ) @ zero_zero_int ) )). + +thf(fact_67_less__special_I4_J,axiom,( + ! [X_1: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_1 ) @ one_one_int ) + <=> ( ord_less_int @ X_1 @ ( bit1 @ pls ) ) ) )). + +thf(fact_68_less__special_I2_J,axiom,( + ! [Y_1: int] : + ( ( ord_less_int @ one_one_int @ ( number_number_of_int @ Y_1 ) ) + <=> ( ord_less_int @ ( bit1 @ pls ) @ Y_1 ) ) )). + +thf(fact_69_odd__less__0,axiom,( + ! [Z: int] : + ( ( ord_less_int @ ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) @ zero_zero_int ) + <=> ( ord_less_int @ Z @ zero_zero_int ) ) )). + +thf(fact_70_double__eq__0__iff,axiom,( + ! [A_5: int] : + ( ( ( plus_plus_int @ A_5 @ A_5 ) + = zero_zero_int ) + <=> ( A_5 = zero_zero_int ) ) )). + +thf(fact_71_rel__simps_I46_J,axiom,( + ! [K: int] : + ( ( bit1 @ K ) + != pls ) )). + +thf(fact_72_rel__simps_I39_J,axiom,( + ! [L: int] : + ( pls + != ( bit1 @ L ) ) )). + +thf(fact_73_rel__simps_I50_J,axiom,( + ! [K: int,L: int] : + ( ( bit1 @ K ) + != ( bit0 @ L ) ) )). + +thf(fact_74_rel__simps_I49_J,axiom,( + ! [K: int,L: int] : + ( ( bit0 @ K ) + != ( bit1 @ L ) ) )). + +thf(fact_75_rel__simps_I44_J,axiom,( + ! [K: int] : + ( ( ( bit0 @ K ) + = pls ) + <=> ( K = pls ) ) )). + +thf(fact_76_rel__simps_I38_J,axiom,( + ! [L: int] : + ( ( pls + = ( bit0 @ L ) ) + <=> ( pls = L ) ) )). + +thf(fact_77_Bit0__Pls,axiom, + ( ( bit0 @ pls ) + = pls )). + +thf(fact_78_Pls__def,axiom,( + pls = zero_zero_int )). + +thf(fact_79_int__0__neq__1,axiom,( + zero_zero_int != one_one_int )). + +thf(fact_80_add__Pls__right,axiom,( + ! [K: int] : + ( ( plus_plus_int @ K @ pls ) + = K ) )). + +thf(fact_81_add__Pls,axiom,( + ! [K: int] : + ( ( plus_plus_int @ pls @ K ) + = K ) )). + +thf(fact_82_add__Bit0__Bit0,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit0 @ L ) ) + = ( bit0 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_83_Bit0__def,axiom,( + ! [K: int] : + ( ( bit0 @ K ) + = ( plus_plus_int @ K @ K ) ) )). + +thf(fact_84_zadd__0__right,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ Z @ zero_zero_int ) + = Z ) )). + +thf(fact_85_zadd__0,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ zero_zero_int @ Z ) + = Z ) )). + +thf(fact_86_semiring__numeral__0__eq__0,axiom, + ( ( number_number_of_int @ pls ) + = zero_zero_int )). + +thf(fact_87_semiring__numeral__0__eq__0,axiom, + ( ( number_number_of_nat @ pls ) + = zero_zero_nat )). + +thf(fact_88_number__of__Pls,axiom, + ( ( number_number_of_int @ pls ) + = zero_zero_int )). + +thf(fact_89_semiring__norm_I112_J,axiom, + ( zero_zero_int + = ( number_number_of_int @ pls ) )). + +thf(fact_90_add__numeral__0,axiom,( + ! [A_4: int] : + ( ( plus_plus_int @ ( number_number_of_int @ pls ) @ A_4 ) + = A_4 ) )). + +thf(fact_91_add__numeral__0__right,axiom,( + ! [A_3: int] : + ( ( plus_plus_int @ A_3 @ ( number_number_of_int @ pls ) ) + = A_3 ) )). + +thf(fact_92_power__eq__0__iff__number__of,axiom,( + ! [A_2: int,W_3: int] : + ( ( ( power_power_int @ A_2 @ ( number_number_of_nat @ W_3 ) ) + = zero_zero_int ) + <=> ( ( A_2 = zero_zero_int ) + & ( ( number_number_of_nat @ W_3 ) + != zero_zero_nat ) ) ) )). + +thf(fact_93_power__eq__0__iff__number__of,axiom,( + ! [A_2: nat,W_3: int] : + ( ( ( power_power_nat @ A_2 @ ( number_number_of_nat @ W_3 ) ) + = zero_zero_nat ) + <=> ( ( A_2 = zero_zero_nat ) + & ( ( number_number_of_nat @ W_3 ) + != zero_zero_nat ) ) ) )). + +thf(fact_94_add__number__of__left,axiom,( + ! [V_2: int,W_2: int,Z_1: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( plus_plus_int @ ( number_number_of_int @ W_2 ) @ Z_1 ) ) + = ( plus_plus_int @ ( number_number_of_int @ ( plus_plus_int @ V_2 @ W_2 ) ) @ Z_1 ) ) )). + +thf(fact_95_add__number__of__eq,axiom,( + ! [V_1: int,W_1: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_1 ) @ ( number_number_of_int @ W_1 ) ) + = ( number_number_of_int @ ( plus_plus_int @ V_1 @ W_1 ) ) ) )). + +thf(fact_96_number__of__add,axiom,( + ! [V: int,W: int] : + ( ( number_number_of_int @ ( plus_plus_int @ V @ W ) ) + = ( plus_plus_int @ ( number_number_of_int @ V ) @ ( number_number_of_int @ W ) ) ) )). + +thf(fact_97_add__Bit1__Bit0,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit1 @ K ) @ ( bit0 @ L ) ) + = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_98_add__Bit0__Bit1,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit1 @ L ) ) + = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_99_Bit1__def,axiom,( + ! [K: int] : + ( ( bit1 @ K ) + = ( plus_plus_int @ ( plus_plus_int @ one_one_int @ K ) @ K ) ) )). + +thf(fact_100_odd__nonzero,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) + != zero_zero_int ) )). + +thf(fact_101_number__of__int,axiom,( + ! [N: nat] : + ( ( number_number_of_nat @ ( semiri1621563631at_int @ N ) ) + = ( semiri984289939at_nat @ N ) ) )). + +thf(fact_102_number__of__int,axiom,( + ! [N: nat] : + ( ( number_number_of_int @ ( semiri1621563631at_int @ N ) ) + = ( semiri1621563631at_int @ N ) ) )). + +thf(fact_103_zero__less__power2,axiom,( + ! [A_1: int] : + ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) + <=> ( A_1 != zero_zero_int ) ) )). + +thf(fact_104_power2__less__0,axiom,( + ! [A: int] : + ~ ( ord_less_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) )). + +thf(fact_105_sum__power2__gt__zero__iff,axiom,( + ! [X: int,Y: int] : + ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) + <=> ( ( X != zero_zero_int ) + | ( Y != zero_zero_int ) ) ) )). + +%----Conjectures (1) +thf(conj_0,conjecture,( + ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + != zero_zero_int )). + +%------------------------------------------------------------------------------ |