include('Axioms/SET010^0.ax').
thf(v7_ordinal1_type, type, v7_ordinal1: $i > $o).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_compos_0_type, type, v1_compos_0: $i > $o).
thf(v2_compos_0_type, type, v2_compos_0: $i > $o).
thf(v3_compos_0_type, type, v3_compos_0: $i > $o).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k3_compos_0_type, type, k3_compos_0: $i > $i > $i).
thf(k2_compos_0_type, type, k2_compos_0: $i > $i > $i).
thf(k5_compos_0_type, type, k5_compos_0: $i > $i > $i > $i).
thf(k2_xtuple_0_type, type, k2_xtuple_0: $i > $i).
thf(k5_xtuple_0_type, type, k5_xtuple_0: $i > $i).
thf(k7_valued_1_type, type, k7_valued_1: $i > $i > $i).
thf(dt_k5_compos_0, axiom,   (! [A: $i, B: $i, C: $i] :  ( ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (v1_compos_0 @ A)  &  ( (v2_compos_0 @ A)  &  (v3_compos_0 @ A) ) ) )  &  ( ( (m1_subset_1 @ B)  @ A)  &  (v7_ordinal1 @ C) ) )  =>  ( (m1_subset_1 @  ( ( (k5_compos_0 @ A)  @ B)  @ C) )  @ A) ) ) , file(compos_0, k5_compos_0)).
thf(d9_compos_0, axiom,   (! [A: $i] :  ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (v1_compos_0 @ A)  &  ( (v2_compos_0 @ A)  &  (v3_compos_0 @ A) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ A)  =>  (! [C: $i] :  ( (v7_ordinal1 @ C)  =>  (! [D: $i] :  ( ( (m1_subset_1 @ D)  @ A)  =>  ( ( (= @ D)  @  ( ( (k5_compos_0 @ A)  @ B)  @ C) )  <=>  ( ( (= @  ( (k2_compos_0 @ A)  @ D) )  @  ( (k2_compos_0 @ A)  @ B) )  &  ( ( (= @  (k2_xtuple_0 @ D) )  @  (k2_xtuple_0 @ B) )  &  ( (= @  (k5_xtuple_0 @ D) )  @  ( (k7_valued_1 @  (k5_xtuple_0 @ B) )  @ C) ) ) ) ) ) ) ) ) ) ) ) ) , file(compos_0, d9_compos_0)).
thf(t5_compos_0, conjecture,   (! [A: $i] :  ( (v7_ordinal1 @ A)  =>  (! [B: $i] :  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( (v1_compos_0 @ B)  &  ( (v2_compos_0 @ B)  &  (v3_compos_0 @ B) ) ) )  =>  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @ B)  =>  ( (= @  ( (k3_compos_0 @ B)  @  ( (k2_compos_0 @ B)  @ C) ) )  @  ( (k3_compos_0 @ B)  @  ( (k2_compos_0 @ B)  @  ( ( (k5_compos_0 @ B)  @ C)  @ A) ) ) ) ) ) ) ) ) ) , file(compos_0, t5_compos_0)).