include('Axioms/SET010^0.ax').
thf(m2_finseq_1_type, type, m2_finseq_1: $i > $i > $o).
thf(k1_numbers_type, type, k1_numbers: $i).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(m2_subset_1_type, type, m2_subset_1: $i > $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(k4_finseq_1_type, type, k4_finseq_1: $i > $i).
thf(k1_seq_1_type, type, k1_seq_1: $i > $i > $i).
thf(k9_real_1_type, type, k9_real_1: $i > $i > $i).
thf(k18_rvsum_1_type, type, k18_rvsum_1: $i > $i).
thf(k7_partfun1_type, type, k7_partfun1: $i > $i > $i > $i).
thf(m1_finseq_1_type, type, m1_finseq_1: $i > $i > $o).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(v1_finseq_1_type, type, v1_finseq_1: $i > $o).
thf(k9_xtuple_0_type, type, k9_xtuple_0: $i > $i).
thf(v3_valued_0_type, type, v3_valued_0: $i > $o).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(v5_relat_1_type, type, v5_relat_1: $i > $i > $o).
thf(k2_finseq_1_type, type, k2_finseq_1: $i > $i).
thf(t22_integra1, axiom,   (! [A: $i] :  ( ( (m2_finseq_1 @ A)  @ k1_numbers)  =>  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @ k1_numbers)  =>  (! [C: $i] :  ( ( (m2_finseq_1 @ C)  @ k1_numbers)  =>  ( ( ( (= @  (k3_finseq_1 @ A) )  @  (k3_finseq_1 @ B) )  &  ( ( (= @  (k3_finseq_1 @ A) )  @  (k3_finseq_1 @ C) )  &  (! [D: $i] :  ( ( ( (m2_subset_1 @ D)  @ k1_numbers)  @ k5_numbers)  =>  ( ( (r2_hidden @ D)  @  (k4_finseq_1 @ A) )  =>  ( (= @  ( (k1_seq_1 @ C)  @ D) )  @  ( (k9_real_1 @  ( ( (k7_partfun1 @ k1_numbers)  @ A)  @ D) )  @  ( ( (k7_partfun1 @ k1_numbers)  @ B)  @ D) ) ) ) ) ) ) )  =>  ( (= @  (k18_rvsum_1 @ C) )  @  ( (k9_real_1 @  (k18_rvsum_1 @ A) )  @  (k18_rvsum_1 @ B) ) ) ) ) ) ) ) ) ) , file(integra1, t22_integra1)).
thf(redefinition_m2_finseq_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @ A)  <=>  ( (m1_finseq_1 @ B)  @ A) ) ) ) , file(finseq_1, m2_finseq_1)).
thf(redefinition_k4_finseq_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v1_finseq_1 @ A) ) )  =>  ( (= @  (k4_finseq_1 @ A) )  @  (k9_xtuple_0 @ A) ) ) ) , file(finseq_1, k4_finseq_1)).
thf(redefinition_k1_seq_1, axiom,   (! [A: $i, B: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v3_valued_0 @ A) ) )  =>  ( (= @  ( (k1_seq_1 @ A)  @ B) )  @  ( (k1_funct_1 @ A)  @ B) ) ) ) , file(seq_1, k1_seq_1)).
thf(dt_m2_finseq_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @ A)  =>  ( (v1_funct_1 @ B)  &  ( (v1_finseq_1 @ B)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ k5_numbers)  @ A) ) ) ) ) ) ) ) , file(finseq_1, m2_finseq_1)).
thf(dt_m1_finseq_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (m1_finseq_1 @ B)  @ A)  =>  ( (v1_relat_1 @ B)  &  ( (v1_funct_1 @ B)  &  (v1_finseq_1 @ B) ) ) ) ) ) , file(finseq_1, m1_finseq_1)).
thf(dt_k3_finseq_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v1_finseq_1 @ A) ) )  =>  ( ( (m2_subset_1 @  (k3_finseq_1 @ A) )  @ k1_numbers)  @ k5_numbers) ) ) , file(finseq_1, k3_finseq_1)).
thf(d6_partfun1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (v1_relat_1 @ B)  &  ( ( (v5_relat_1 @ B)  @ A)  &  (v1_funct_1 @ B) ) )  =>  (! [C: $i] :  ( ( (r2_hidden @ C)  @  (k9_xtuple_0 @ B) )  =>  ( (= @  ( ( (k7_partfun1 @ A)  @ B)  @ C) )  @  ( (k1_funct_1 @ B)  @ C) ) ) ) ) ) ) , file(partfun1, d6_partfun1)).
thf(d3_finseq_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v1_finseq_1 @ A) ) )  =>  (! [B: $i] :  ( ( ( (m2_subset_1 @ B)  @ k1_numbers)  @ k5_numbers)  =>  ( ( (= @ B)  @  (k3_finseq_1 @ A) )  <=>  ( (= @  (k2_finseq_1 @ B) )  @  (k9_xtuple_0 @ A) ) ) ) ) ) ) , file(finseq_1, d3_finseq_1)).
thf(cc4_seqm_3, axiom,   (! [A: $i] :  ( ( (m1_finseq_1 @ A)  @ k1_numbers)  =>  (v3_valued_0 @ A) ) ) , file(seqm_3, cc4_seqm_3)).
thf(cc3_finseq_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (m1_finseq_1 @ B)  @ A)  =>  ( (v5_relat_1 @ B)  @ A) ) ) ) , file(finseq_1, cc3_finseq_1)).
thf(t8_entropy1, conjecture,   (! [A: $i] :  ( ( (m2_finseq_1 @ A)  @ k1_numbers)  =>  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @ k1_numbers)  =>  (! [C: $i] :  ( ( (m2_finseq_1 @ C)  @ k1_numbers)  =>  ( ( ( (= @  (k3_finseq_1 @ B) )  @  (k3_finseq_1 @ A) )  &  ( ( (= @  (k3_finseq_1 @ B) )  @  (k3_finseq_1 @ C) )  &  (! [D: $i] :  ( ( ( (m2_subset_1 @ D)  @ k1_numbers)  @ k5_numbers)  =>  ( ( (r2_hidden @ D)  @  (k4_finseq_1 @ B) )  =>  ( (= @  ( (k1_seq_1 @ A)  @ D) )  @  ( (k9_real_1 @  ( (k1_seq_1 @ B)  @ D) )  @  ( (k1_seq_1 @ C)  @ D) ) ) ) ) ) ) )  =>  ( (= @  (k18_rvsum_1 @ A) )  @  ( (k9_real_1 @  (k18_rvsum_1 @ B) )  @  (k18_rvsum_1 @ C) ) ) ) ) ) ) ) ) ) , file(entropy1, t8_entropy1)).