%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:11:49 EDT 2023 % Result : Theorem 45.68s 6.93s % Output : Proof 75.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.06/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n005.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Sun Aug 27 13:05:08 EDT 2023 % 0.12/0.35 % CPUTime : % 0.19/0.68 ________ _____ % 0.19/0.68 ___ __ \_________(_)________________________________ % 0.19/0.68 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.68 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.68 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.68 % 0.19/0.68 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.68 (2023-06-19) % 0.19/0.68 % 0.19/0.68 (c) Philipp Rümmer, 2009-2023 % 0.19/0.68 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.68 Amanda Stjerna. % 0.19/0.68 Free software under BSD-3-Clause. % 0.19/0.68 % 0.19/0.68 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.68 % 0.19/0.68 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.73/0.71 Running up to 7 provers in parallel. % 0.73/0.73 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.73/0.73 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.73/0.73 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.73/0.73 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.73/0.73 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.73/0.73 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.73/0.73 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 14.32/2.81 Prover 1: Preprocessing ... % 15.04/2.86 Prover 4: Preprocessing ... % 15.04/2.88 Prover 6: Preprocessing ... % 15.04/2.88 Prover 3: Preprocessing ... % 15.04/2.88 Prover 2: Preprocessing ... % 16.05/2.96 Prover 0: Preprocessing ... % 16.11/2.98 Prover 5: Preprocessing ... % 36.37/5.68 Prover 1: Warning: ignoring some quantifiers % 36.37/5.74 Prover 3: Warning: ignoring some quantifiers % 36.37/5.81 Prover 6: Proving ... % 36.37/5.82 Prover 3: Constructing countermodel ... % 38.17/5.91 Prover 1: Constructing countermodel ... % 38.65/5.96 Prover 4: Warning: ignoring some quantifiers % 40.08/6.16 Prover 4: Constructing countermodel ... % 41.99/6.46 Prover 0: Proving ... % 45.68/6.93 Prover 3: proved (6201ms) % 45.68/6.93 % 45.68/6.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 45.68/6.93 % 45.68/6.93 Prover 6: stopped % 46.15/6.95 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 46.15/6.95 Prover 0: stopped % 46.31/6.97 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 46.31/6.97 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 48.19/7.24 Prover 5: Proving ... % 48.19/7.24 Prover 5: stopped % 48.19/7.25 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 53.41/7.92 Prover 7: Preprocessing ... % 53.41/7.94 Prover 8: Preprocessing ... % 54.03/7.99 Prover 10: Preprocessing ... % 55.09/8.19 Prover 2: Proving ... % 55.09/8.19 Prover 2: stopped % 55.77/8.21 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 55.77/8.31 Prover 11: Preprocessing ... % 60.62/8.90 Prover 13: Preprocessing ... % 63.78/9.29 Prover 10: Warning: ignoring some quantifiers % 65.50/9.50 Prover 10: Constructing countermodel ... % 65.90/9.53 Prover 8: Warning: ignoring some quantifiers % 66.49/9.65 Prover 8: Constructing countermodel ... % 68.97/9.94 Prover 7: Warning: ignoring some quantifiers % 70.14/10.12 Prover 7: Constructing countermodel ... % 70.95/10.22 Prover 11: Warning: ignoring some quantifiers % 70.95/10.28 Prover 1: Found proof (size 215) % 70.95/10.28 Prover 1: proved (9554ms) % 70.95/10.28 Prover 8: stopped % 70.95/10.28 Prover 10: stopped % 70.95/10.28 Prover 4: stopped % 70.95/10.30 Prover 7: stopped % 72.09/10.37 Prover 11: Constructing countermodel ... % 72.09/10.38 Prover 11: stopped % 72.63/10.51 Prover 13: Warning: ignoring some quantifiers % 73.25/10.64 Prover 13: Constructing countermodel ... % 73.33/10.64 Prover 13: stopped % 73.33/10.64 % 73.33/10.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 73.33/10.65 % 73.63/10.75 % SZS output start Proof for theBenchmark % 73.85/10.77 Assumptions after simplification: % 73.85/10.77 --------------------------------- % 73.85/10.77 % 73.85/10.77 (axiom171) % 73.85/10.79 Nat_int_fun$(of_nat$) & A_iarray_list_nat_fun$(size$) & ! [v0: Nat$] : ! % 73.85/10.79 [v1: A_iarray_list$] : ! [v2: A_iarray_list_nat_fun$] : ! [v3: Nat$] : ( ~ % 73.85/10.79 (gen_length$b(v0) = v2) | ~ (fun_app$m(v2, v1) = v3) | ~ % 73.85/10.79 A_iarray_list$(v1) | ~ Nat$(v0) | ? [v4: int] : ? [v5: int] : ? [v6: % 73.85/10.79 Nat$] : (fun_app$m(size$, v1) = v6 & fun_app$l(of_nat$, v6) = % 73.85/10.79 $difference(v4, v5) & fun_app$l(of_nat$, v3) = v4 & fun_app$l(of_nat$, v0) % 73.85/10.79 = v5 & Nat$(v6))) % 73.85/10.79 % 73.85/10.79 (axiom176) % 73.85/10.79 Nat_int_fun$(of_nat$) & A_iarray_list_nat_fun$(size$) & ! [v0: % 73.85/10.79 A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: Nat$] : ! [v3: Nat$] : % 73.85/10.79 ( ~ (fun_app$m(size$, v1) = v3) | ~ (fun_app$m(size$, v0) = v2) | ~ % 73.85/10.79 A_iarray_list$(v1) | ~ A_iarray_list$(v0) | ? [v4: A_iarray_list$] : ? % 73.85/10.79 [v5: Nat$] : ? [v6: int] : ? [v7: int] : (splice$b(v0, v1) = v4 & % 73.85/10.79 fun_app$m(size$, v4) = v5 & fun_app$l(of_nat$, v5) = v6 & % 73.85/10.79 fun_app$l(of_nat$, v3) = $difference(v6, v7) & fun_app$l(of_nat$, v2) = v7 % 73.85/10.79 & A_iarray_list$(v4) & Nat$(v5))) % 73.85/10.79 % 73.85/10.79 (axiom27) % 73.85/10.79 Nat_int_fun$(of_nat$) & A_iarray_bool_fun$(uu$) & % 73.85/10.79 A_iarray_list_nat_fun$(size$) & A_iarray_iarray_nat_fun$(rank_iarray$) & ? % 73.85/10.79 [v0: A_iarray_list_a_iarray_list_fun$] : (filter$(uu$) = v0 & % 73.85/10.79 A_iarray_list_a_iarray_list_fun$(v0) & ! [v1: A_iarray_iarray$] : ! [v2: % 73.85/10.79 Nat$] : ( ~ (fun_app$q(rank_iarray$, v1) = v2) | ~ A_iarray_iarray$(v1) | % 73.85/10.79 ? [v3: int] : ? [v4: A_iarray_iarray$] : ? [v5: A_iarray_list$] : ? % 73.85/10.79 [v6: A_iarray_list$] : ? [v7: Nat$] : (gauss_Jordan_iarrays$(v1) = v4 & % 73.85/10.79 list_of$(v4) = v5 & fun_app$p(v0, v5) = v6 & fun_app$m(size$, v6) = v7 & % 73.85/10.79 fun_app$l(of_nat$, v7) = v3 & fun_app$l(of_nat$, v2) = v3 & % 73.85/10.79 A_iarray_list$(v6) & A_iarray_list$(v5) & Nat$(v7) & % 73.85/10.79 A_iarray_iarray$(v4)))) % 73.85/10.79 % 73.85/10.79 (axiom28) % 73.85/10.80 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ (gauss_Jordan$(v0) = % 73.85/10.80 v1) | ~ A_n_vec_n_vec$(v0) | ? [v2: A_iarray_iarray$] : ? [v3: % 73.85/10.80 A_iarray_iarray$] : (matrix_to_iarray$(v1) = v2 & matrix_to_iarray$(v0) = % 73.85/10.80 v3 & gauss_Jordan_iarrays$(v3) = v2 & A_iarray_iarray$(v3) & % 73.85/10.80 A_iarray_iarray$(v2))) % 73.85/10.80 % 73.85/10.80 (axiom418) % 73.85/10.80 Int_nat_fun$(nat$) & Nat_a_iarray_prod_list_nat_fun$(size$a) & ? [v0: Nat$] : % 73.85/10.80 (gen_length$(v0) = size$a & fun_app$k(nat$, 0) = v0 & Nat$(v0)) % 73.85/10.80 % 73.85/10.80 (axiom419) % 73.85/10.80 A_iarray_list_list_nat_fun$(size$b) & Int_nat_fun$(nat$) & ? [v0: Nat$] : % 73.85/10.80 (gen_length$a(v0) = size$b & fun_app$k(nat$, 0) = v0 & Nat$(v0)) % 73.85/10.80 % 73.85/10.80 (axiom420) % 73.85/10.80 Int_nat_fun$(nat$) & A_iarray_list_nat_fun$(size$) & ? [v0: Nat$] : % 73.85/10.80 (gen_length$b(v0) = size$ & fun_app$k(nat$, 0) = v0 & Nat$(v0)) % 73.85/10.80 % 73.85/10.80 (axiom422) % 73.85/10.80 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.80 0) = v0 & Nat$(v0) & ! [v1: Nat_nat_bool_fun_fun$] : ! [v2: Nat$] : ! % 73.85/10.80 [v3: Nat$] : ! [v4: Nat_bool_fun$] : ! [v5: int] : (v5 = 0 | ~ % 73.85/10.80 (fun_app$as(v1, v2) = v4) | ~ (fun_app$c(v4, v3) = v5) | ~ Nat$(v3) | ~ % 73.85/10.80 Nat$(v2) | ~ Nat_nat_bool_fun_fun$(v1) | ? [v6: Nat$] : ? [v7: Nat$] : % 73.85/10.80 ? [v8: Nat_bool_fun$] : ? [v9: int] : ? [v10: int] : ? [v11: Nat$] : ? % 73.85/10.80 [v12: int] : ( ~ (v12 = 0) & fun_app$as(v1, v6) = v8 & fun_app$l(of_nat$, % 73.85/10.80 v7) = v10 & fun_app$l(of_nat$, v6) = v9 & fun_app$k(nat$, $sum(v10, % 73.85/10.80 v9)) = v11 & fun_app$c(v8, v11) = v12 & fun_app$c(v8, v7) = 0 & % 73.85/10.80 Nat_bool_fun$(v8) & Nat$(v11) & Nat$(v7) & Nat$(v6)) | ? [v6: Nat$] : % 73.85/10.80 ? [v7: Nat$] : ? [v8: Nat_bool_fun$] : ? [v9: any] : ? [v10: % 73.85/10.80 Nat_bool_fun$] : ? [v11: any] : (fun_app$as(v1, v7) = v10 & % 73.85/10.80 fun_app$as(v1, v6) = v8 & fun_app$c(v10, v6) = v11 & fun_app$c(v8, v7) = % 73.85/10.80 v9 & Nat_bool_fun$(v10) & Nat_bool_fun$(v8) & Nat$(v7) & Nat$(v6) & ( ~ % 73.85/10.80 (v11 = 0) | ~ (v9 = 0)) & (v11 = 0 | v9 = 0)) | ? [v6: Nat$] : ? % 73.85/10.80 [v7: Nat_bool_fun$] : ? [v8: int] : ( ~ (v8 = 0) & fun_app$as(v1, v6) = % 73.85/10.80 v7 & fun_app$c(v7, v0) = v8 & Nat_bool_fun$(v7) & Nat$(v6)))) % 73.85/10.80 % 73.85/10.80 (axiom451) % 73.85/10.80 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.80 0) = v0 & Nat$(v0) & ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : ( ~ % 73.85/10.80 (fun_app$c(v1, v2) = 0) | ~ Nat_bool_fun$(v1) | ~ Nat$(v2) | % 73.85/10.80 fun_app$c(v1, v0) = 0 | ? [v3: Nat$] : ? [v4: int] : ? [v5: Nat$] : ? % 73.85/10.80 [v6: int] : ( ~ (v6 = 0) & fun_app$l(of_nat$, v3) = v4 & fun_app$k(nat$, % 73.85/10.80 $sum(v4, 1)) = v5 & fun_app$c(v1, v5) = 0 & fun_app$c(v1, v3) = v6 & % 73.85/10.80 Nat$(v5) & Nat$(v3)))) % 73.85/10.80 % 73.85/10.81 (axiom452) % 73.85/10.81 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.81 0) = v0 & Nat$(v0) & ! [v1: Nat_nat_bool_fun_fun$] : ! [v2: Nat$] : ! % 73.85/10.81 [v3: Nat$] : ! [v4: Nat_bool_fun$] : ! [v5: int] : (v5 = 0 | ~ % 73.85/10.81 (fun_app$as(v1, v2) = v4) | ~ (fun_app$c(v4, v3) = v5) | ~ Nat$(v3) | ~ % 73.85/10.81 Nat$(v2) | ~ Nat_nat_bool_fun_fun$(v1) | ? [v6: Nat$] : ? [v7: Nat$] : % 73.85/10.81 ? [v8: Nat_bool_fun$] : ? [v9: int] : ? [v10: Nat$] : ? [v11: % 73.85/10.81 Nat_bool_fun$] : ? [v12: int] : ? [v13: Nat$] : ? [v14: int] : ( ~ % 73.85/10.81 (v14 = 0) & fun_app$as(v1, v10) = v11 & fun_app$as(v1, v6) = v8 & % 73.85/10.81 fun_app$l(of_nat$, v7) = v12 & fun_app$l(of_nat$, v6) = v9 & % 73.85/10.81 fun_app$k(nat$, $sum(v12, 1)) = v13 & fun_app$k(nat$, $sum(v9, 1)) = v10 % 73.85/10.81 & fun_app$c(v11, v13) = v14 & fun_app$c(v8, v7) = 0 & Nat_bool_fun$(v11) % 73.85/10.81 & Nat_bool_fun$(v8) & Nat$(v13) & Nat$(v10) & Nat$(v7) & Nat$(v6)) | ? % 73.85/10.81 [v6: Nat$] : ? [v7: Nat_bool_fun$] : ? [v8: int] : ( ~ (v8 = 0) & % 73.85/10.81 fun_app$as(v1, v6) = v7 & fun_app$c(v7, v0) = v8 & Nat_bool_fun$(v7) & % 73.85/10.81 Nat$(v6)) | ? [v6: Nat_bool_fun$] : (fun_app$as(v1, v0) = v6 & % 73.85/10.81 Nat_bool_fun$(v6) & ? [v7: Nat$] : ? [v8: int] : ? [v9: Nat$] : ? % 73.85/10.81 [v10: int] : ( ~ (v10 = 0) & fun_app$l(of_nat$, v7) = v8 & % 73.85/10.81 fun_app$k(nat$, $sum(v8, 1)) = v9 & fun_app$c(v6, v9) = v10 & Nat$(v9) % 73.85/10.81 & Nat$(v7))))) % 73.85/10.81 % 73.85/10.81 (axiom453) % 73.85/10.81 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.81 0) = v0 & Nat$(v0) & ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : ! [v3: int] % 73.85/10.81 : (v3 = 0 | ~ (fun_app$c(v1, v2) = v3) | ~ Nat_bool_fun$(v1) | ~ Nat$(v2) % 73.85/10.81 | ? [v4: Nat$] : ? [v5: int] : ? [v6: Nat$] : ? [v7: int] : ( ~ (v7 = % 73.85/10.81 0) & fun_app$l(of_nat$, v4) = v5 & fun_app$k(nat$, $sum(v5, 1)) = v6 & % 73.85/10.81 fun_app$c(v1, v6) = v7 & fun_app$c(v1, v4) = 0 & Nat$(v6) & Nat$(v4)) | % 73.85/10.81 ? [v4: int] : ( ~ (v4 = 0) & fun_app$c(v1, v0) = v4))) % 73.85/10.81 % 73.85/10.81 (axiom585) % 73.85/10.81 Nat_int_fun$(of_nat$) & A_iarray_list$(nil$) & A_iarray_list_nat_fun$(size$) & % 73.85/10.81 ? [v0: Nat$] : (fun_app$m(size$, nil$) = v0 & fun_app$l(of_nat$, v0) = 0 & % 73.85/10.81 Nat$(v0)) % 73.85/10.81 % 73.85/10.81 (axiom625) % 73.85/10.81 Nat_int_fun$(of_nat$) & A_iarray_list$(nil$) & A_iarray_list_nat_fun$(size$) & % 73.85/10.81 ! [v0: A_iarray_list$] : ! [v1: Nat$] : (v0 = nil$ | ~ (fun_app$m(size$, % 73.85/10.81 v0) = v1) | ~ A_iarray_list$(v0) | ? [v2: int] : ($lesseq(1, v2) & % 73.85/10.81 fun_app$l(of_nat$, v1) = v2)) & ! [v0: Nat$] : ( ~ (fun_app$m(size$, % 73.85/10.81 nil$) = v0) | ? [v1: int] : ($lesseq(v1, 0)fun_app$l(of_nat$, v0) = % 73.85/10.81 v1)) % 73.85/10.81 % 73.85/10.81 (axiom631) % 73.85/10.82 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.82 0) = v0 & Nat$(v0) & ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : ! [v3: int] % 73.85/10.82 : ! [v4: any] : ( ~ (fun_app$l(of_nat$, v1) = v3) | ~ (fun_app$c(v2, v0) = % 73.85/10.82 v4) | ~ Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: Nat$] : ? [v6: int] % 73.85/10.82 : ? [v7: int] : ( ~ (v7 = 0) & $lesseq(v6, v3) & fun_app$l(of_nat$, v5) = % 73.85/10.82 v6 & fun_app$c(v2, v5) = v7 & Nat$(v5)) | (v4 = 0 & ! [v5: Nat$] : ! % 73.85/10.82 [v6: int] : ! [v7: Nat$] : ! [v8: int] : (v8 = 0 | ~ ($lesseq(1, % 73.85/10.82 $difference(v3, v6))) | ~ (fun_app$l(of_nat$, v5) = v6) | ~ % 73.85/10.82 (fun_app$k(nat$, $sum(v6, 1)) = v7) | ~ (fun_app$c(v2, v7) = v8) | ~ % 73.85/10.82 Nat$(v5)))) & ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : ! [v3: int] : % 73.85/10.82 ( ~ (fun_app$l(of_nat$, v1) = v3) | ~ (fun_app$c(v2, v0) = 0) | ~ % 73.85/10.82 Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v4: Nat$] : ? [v5: int] : ? [v6: % 73.85/10.82 Nat$] : ? [v7: int] : ( ~ (v7 = 0) & $lesseq(1, $difference(v3, v5)) & % 73.85/10.82 fun_app$l(of_nat$, v4) = v5 & fun_app$k(nat$, $sum(v5, 1)) = v6 & % 73.85/10.82 fun_app$c(v2, v6) = v7 & Nat$(v6) & Nat$(v4)) | ! [v4: Nat$] : ! [v5: % 73.85/10.82 int] : ( ~ ($lesseq(v5, v3)) | ~ (fun_app$l(of_nat$, v4) = v5) | ~ % 73.85/10.82 Nat$(v4) | fun_app$c(v2, v4) = 0))) % 73.85/10.82 % 73.85/10.82 (axiom633) % 73.85/10.82 Nat_int_fun$(of_nat$) & Int_nat_fun$(nat$) & ? [v0: Nat$] : (fun_app$k(nat$, % 73.85/10.82 0) = v0 & Nat$(v0) & ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : ! [v3: int] % 73.85/10.82 : ! [v4: int] : (v4 = 0 | ~ (fun_app$l(of_nat$, v1) = v3) | ~ % 73.85/10.82 (fun_app$c(v2, v0) = v4) | ~ Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: % 73.85/10.82 Nat$] : ? [v6: int] : ? [v7: Nat$] : ($lesseq(1, $difference(v3, v6)) % 73.85/10.82 & fun_app$l(of_nat$, v5) = v6 & fun_app$k(nat$, $sum(v6, 1)) = v7 & % 73.85/10.82 fun_app$c(v2, v7) = 0 & Nat$(v7) & Nat$(v5)) | ! [v5: Nat$] : ! [v6: % 73.85/10.82 int] : ( ~ ($lesseq(v6, v3)) | ~ (fun_app$l(of_nat$, v5) = v6) | ~ % 73.85/10.82 Nat$(v5) | ? [v7: int] : ( ~ (v7 = 0) & fun_app$c(v2, v5) = v7))) & ! % 73.85/10.82 [v1: Nat$] : ! [v2: Nat_bool_fun$] : ! [v3: any] : ! [v4: int] : ( ~ % 73.85/10.82 (fun_app$l(of_nat$, v1) = v4) | ~ (fun_app$c(v2, v0) = v3) | ~ % 73.85/10.82 Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: Nat$] : ? [v6: int] : % 73.85/10.82 ($lesseq(v6, v4) & fun_app$l(of_nat$, v5) = v6 & fun_app$c(v2, v5) = 0 & % 73.85/10.82 Nat$(v5)) | ( ~ (v3 = 0) & ! [v5: Nat$] : ! [v6: int] : ! [v7: Nat$] % 73.85/10.82 : ( ~ ($lesseq(1, $difference(v4, v6))) | ~ (fun_app$l(of_nat$, v5) = % 73.85/10.82 v6) | ~ (fun_app$k(nat$, $sum(v6, 1)) = v7) | ~ (fun_app$c(v2, v7) % 73.85/10.82 = 0) | ~ Nat$(v5))))) % 73.85/10.82 % 73.85/10.82 (axiom636) % 73.85/10.82 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: % 73.85/10.82 int] : ( ~ ($lesseq(1, $difference(v2, v3))) | ~ (fun_app$l(of_nat$, v1) = % 73.85/10.82 v2) | ~ (fun_app$l(of_nat$, v0) = v3) | ~ Nat$(v1) | ~ Nat$(v0) | ? % 73.85/10.82 [v4: Nat$] : (fun_app$l(of_nat$, v4) = $sum($difference(v2, v3), -1) & % 73.85/10.82 Nat$(v4))) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: int] : % 73.85/10.82 ( ~ ($lesseq(v2, v3)) | ~ (fun_app$l(of_nat$, v1) = v2) | ~ % 73.85/10.82 (fun_app$l(of_nat$, v0) = v3) | ~ Nat$(v1) | ~ Nat$(v0) | ! [v4: Nat$] : % 73.85/10.82 ( ~ (fun_app$l(of_nat$, v4) = $sum($difference(v2, v3), -1)) | ~ Nat$(v4))) % 73.85/10.82 % 73.85/10.82 (axiom638) % 73.85/10.82 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: % 73.85/10.82 int] : ( ~ ($lesseq(v3, -1)) | ~ (fun_app$l(of_nat$, v1) = v3) | ~ % 73.85/10.82 (fun_app$l(of_nat$, v0) = v2) | ~ Nat$(v1) | ~ Nat$(v0)) % 73.85/10.82 % 73.85/10.82 (conjecture22) % 73.85/10.83 Nat_int_fun$(of_nat$) & A_iarray_iarray_option$(none$) & % 73.85/10.83 A_iarray_bool_fun$(uu$) & % 73.85/10.83 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_fun$(fst$) & % 73.85/10.83 A_iarray_list_nat_fun$(size$) & A_n_vec_n_vec$(a$) & % 73.85/10.83 A_iarray_iarray_nat_fun$(nrows_iarray$) & ? [v0: % 73.85/10.83 A_iarray_list_a_iarray_list_fun$] : ? [v1: A_iarray_iarray$] : ? [v2: % 73.85/10.83 A_iarray_iarray$] : ? [v3: A_iarray_list$] : ? [v4: A_iarray_list$] : ? % 73.85/10.83 [v5: Nat$] : ? [v6: int] : ? [v7: Nat$] : ? [v8: int] : ? [v9: % 73.85/10.83 A_n_vec_n_vec$] : ? [v10: A_iarray_iarray$] : ? [v11: A_iarray_list$] : ? % 73.85/10.83 [v12: A_iarray_list$] : ? [v13: Nat$] : ? [v14: int] : ? [v15: % 73.85/10.83 A_iarray_iarray_a_iarray_iarray_prod$] : ? [v16: A_iarray_iarray$] : ? % 73.85/10.83 [v17: A_iarray_iarray_option$] : (gauss_Jordan_iarrays_PA$(v1) = v15 & % 73.85/10.83 fun_app$r(fst$, v15) = v16 & gauss_Jordan$(a$) = v9 & matrix_to_iarray$(v9) % 73.85/10.83 = v10 & matrix_to_iarray$(a$) = v1 & filter$(uu$) = v0 & % 73.85/10.83 fun_app$q(nrows_iarray$, v1) = v7 & gauss_Jordan_iarrays$(v1) = v2 & % 73.85/10.83 list_of$(v10) = v11 & list_of$(v2) = v3 & fun_app$p(v0, v11) = v12 & % 73.85/10.83 fun_app$p(v0, v3) = v4 & some$(v16) = v17 & fun_app$m(size$, v12) = v13 & % 73.85/10.83 fun_app$m(size$, v4) = v5 & fun_app$l(of_nat$, v13) = v14 & % 73.85/10.83 fun_app$l(of_nat$, v7) = v8 & fun_app$l(of_nat$, v5) = v6 & % 73.85/10.83 A_iarray_list_a_iarray_list_fun$(v0) & A_iarray_list$(v12) & % 73.85/10.83 A_iarray_list$(v11) & A_iarray_list$(v4) & A_iarray_list$(v3) & % 73.85/10.83 A_iarray_iarray_option$(v17) & Nat$(v13) & Nat$(v7) & Nat$(v5) & % 73.85/10.83 A_n_vec_n_vec$(v9) & A_iarray_iarray$(v16) & A_iarray_iarray$(v10) & % 73.85/10.83 A_iarray_iarray$(v2) & A_iarray_iarray$(v1) & % 73.85/10.83 A_iarray_iarray_a_iarray_iarray_prod$(v15) & ((v14 = v8 & ~ (v17 = none$) & % 73.85/10.83 ~ (v8 = v6)) | (v8 = v6 & ~ (v17 = none$) & ~ (v14 = v6)))) % 73.85/10.83 % 73.85/10.83 (function-axioms) % 74.23/10.90 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.90 Int_int_prod_int_int_prod_fun$] : ! [v3: Int_int_prod_int_int_prod_fun$] : % 74.23/10.90 ! [v4: Int_int_prod_int_fun$] : ! [v5: Int_int_prod_int_fun$] : ! [v6: % 74.23/10.90 Int_int_prod_set$] : (v1 = v0 | ~ (csquare$b(v6, v5, v4, v3, v2) = v1) | ~ % 74.23/10.90 (csquare$b(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.90 MultipleValueBool] : ! [v2: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.90 : ! [v3: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.90 : ! [v4: A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_fun$] : ! [v5: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_fun$] : ! [v6: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (csquare$a(v6, % 74.23/10.90 v5, v4, v3, v2) = v1) | ~ (csquare$a(v6, v5, v4, v3, v2) = v0)) & ! % 74.23/10.90 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : ! % 74.23/10.90 [v3: A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : % 74.23/10.90 ! [v4: A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_fun$] : ! [v5: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_fun$] : ! [v6: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod_set$] : (v1 = v0 | ~ (csquare$(v6, v5, v4, % 74.23/10.90 v3, v2) = v1) | ~ (csquare$(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 74.23/10.90 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: A_iarray_iarray$] : % 74.23/10.90 ! [v3: A_iarray_iarray$] : ! [v4: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v5: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.90 (pick_middlep$(v5, v4, v3, v2) = v1) | ~ (pick_middlep$(v5, v4, v3, v2) = % 74.23/10.90 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v3: A_iarray_iarray_nat_fun$] : % 74.23/10.90 ! [v4: A_iarray_iarray_nat_fun$] : (v1 = v0 | ~ (size_prod$b(v4, v3, v2) = % 74.23/10.90 v1) | ~ (size_prod$b(v4, v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : % 74.23/10.90 ! [v2: Int_int_prod$] : ! [v3: Int_nat_fun$] : ! [v4: Int_nat_fun$] : (v1 = % 74.23/10.90 v0 | ~ (size_prod$a(v4, v3, v2) = v1) | ~ (size_prod$a(v4, v3, v2) = v0)) % 74.23/10.90 & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : % 74.23/10.90 ! [v3: A_n_vec_n_vec_nat_fun$] : ! [v4: A_n_vec_n_vec_nat_fun$] : (v1 = v0 | % 74.23/10.90 ~ (size_prod$(v4, v3, v2) = v1) | ~ (size_prod$(v4, v3, v2) = v0)) & ! % 74.23/10.90 [v0: A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.90 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: Nat_a_iarray_list_fun$] : % 74.23/10.90 ! [v3: Nat_a_iarray_list_fun$] : ! [v4: Nat_set$] : (v1 = v0 | ~ % 74.23/10.90 (image2$i(v4, v3, v2) = v1) | ~ (image2$i(v4, v3, v2) = v0)) & ! [v0: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v1: % 74.23/10.90 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v2: % 74.23/10.90 Int_a_iarray_iarray_fun$] : ! [v3: Int_a_iarray_iarray_fun$] : ! [v4: % 74.23/10.90 Int_set$] : (v1 = v0 | ~ (image2$h(v4, v3, v2) = v1) | ~ (image2$h(v4, v3, % 74.23/10.90 v2) = v0)) & ! [v0: A_iarray_iarray_a_iarray_iarray_prod_set$] : ! % 74.23/10.90 [v1: A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v2: % 74.23/10.90 Nat_a_iarray_iarray_fun$] : ! [v3: Nat_a_iarray_iarray_fun$] : ! [v4: % 74.23/10.90 Nat_set$] : (v1 = v0 | ~ (image2$g(v4, v3, v2) = v1) | ~ (image2$g(v4, v3, % 74.23/10.90 v2) = v0)) & ! [v0: A_iarray_a_iarray_prod_set$] : ! [v1: % 74.23/10.90 A_iarray_a_iarray_prod_set$] : ! [v2: A_iarray_a_iarray_fun$] : ! [v3: % 74.23/10.90 A_iarray_a_iarray_fun$] : ! [v4: A_iarray_set$] : (v1 = v0 | ~ % 74.23/10.90 (image2$f(v4, v3, v2) = v1) | ~ (image2$f(v4, v3, v2) = v0)) & ! [v0: % 74.23/10.90 A_iarray_a_iarray_prod_set$] : ! [v1: A_iarray_a_iarray_prod_set$] : ! % 74.23/10.90 [v2: Int_a_iarray_fun$] : ! [v3: Int_a_iarray_fun$] : ! [v4: Int_set$] : (v1 % 74.23/10.90 = v0 | ~ (image2$e(v4, v3, v2) = v1) | ~ (image2$e(v4, v3, v2) = v0)) & ! % 74.23/10.90 [v0: A_iarray_a_iarray_prod_set$] : ! [v1: A_iarray_a_iarray_prod_set$] : ! % 74.23/10.90 [v2: Nat_a_iarray_fun$] : ! [v3: Nat_a_iarray_fun$] : ! [v4: Nat_set$] : (v1 % 74.23/10.90 = v0 | ~ (image2$d(v4, v3, v2) = v1) | ~ (image2$d(v4, v3, v2) = v0)) & ! % 74.23/10.90 [v0: Int_int_prod_set$] : ! [v1: Int_int_prod_set$] : ! [v2: % 74.23/10.90 A_iarray_list_int_fun$] : ! [v3: A_iarray_list_int_fun$] : ! [v4: % 74.23/10.90 A_iarray_list_set$] : (v1 = v0 | ~ (image2$c(v4, v3, v2) = v1) | ~ % 74.23/10.90 (image2$c(v4, v3, v2) = v0)) & ! [v0: Int_int_prod_set$] : ! [v1: % 74.23/10.90 Int_int_prod_set$] : ! [v2: A_iarray_int_fun$] : ! [v3: A_iarray_int_fun$] % 74.23/10.90 : ! [v4: A_iarray_set$] : (v1 = v0 | ~ (image2$b(v4, v3, v2) = v1) | ~ % 74.23/10.90 (image2$b(v4, v3, v2) = v0)) & ! [v0: Int_int_prod_set$] : ! [v1: % 74.23/10.90 Int_int_prod_set$] : ! [v2: Int_int_fun$] : ! [v3: Int_int_fun$] : ! [v4: % 74.23/10.90 Int_set$] : (v1 = v0 | ~ (image2$a(v4, v3, v2) = v1) | ~ (image2$a(v4, v3, % 74.23/10.90 v2) = v0)) & ! [v0: Int_int_prod_set$] : ! [v1: Int_int_prod_set$] : % 74.23/10.90 ! [v2: Nat_int_fun$] : ! [v3: Nat_int_fun$] : ! [v4: Nat_set$] : (v1 = v0 | % 74.23/10.90 ~ (image2$(v4, v3, v2) = v1) | ~ (image2$(v4, v3, v2) = v0)) & ! [v0: % 74.23/10.90 Int_int_fun$] : ! [v1: Int_int_fun$] : ! [v2: int] : ! [v3: % 74.23/10.90 Int_int_bool_fun_fun$] : ! [v4: Int_int_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.90 (pick_middlep$a(v4, v3, v2) = v1) | ~ (pick_middlep$a(v4, v3, v2) = v0)) & % 74.23/10.90 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : % 74.23/10.90 ! [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan_in_ij$(v4, v3, v2) = v1) % 74.23/10.90 | ~ (gauss_Jordan_in_ij$(v4, v3, v2) = v0)) & ! [v0: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v1: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 74.23/10.90 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : (v1 = v0 | ~ % 74.23/10.90 (gauss_Jordan_in_ij_PA$(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij_PA$(v4, % 74.23/10.90 v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 74.23/10.90 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_bool_fun$] : ! [v4: % 74.23/10.90 tlbool] : (v1 = v0 | ~ (def_6(v4, v3, v2) = v1) | ~ (def_6(v4, v3, v2) = % 74.23/10.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 74.23/10.90 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_bool_fun$] : ! [v4: % 74.23/10.90 tlbool] : (v1 = v0 | ~ (def_4(v4, v3, v2) = v1) | ~ (def_4(v4, v3, v2) = % 74.23/10.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 74.23/10.90 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_bool_fun$] : ! [v4: % 74.23/10.90 tlbool] : (v1 = v0 | ~ (def_2(v4, v3, v2) = v1) | ~ (def_2(v4, v3, v2) = % 74.23/10.90 v0)) & ! [v0: A_iarray_list_list$] : ! [v1: A_iarray_list_list$] : ! % 74.23/10.90 [v2: A_iarray_list$] : ! [v3: Nat$] : (v1 = v0 | ~ (n_lists$(v3, v2) = v1) | % 74.23/10.90 ~ (n_lists$(v3, v2) = v0)) & ! [v0: A_iarray_list$] : ! [v1: % 74.23/10.90 A_iarray_list$] : ! [v2: Nat_set$] : ! [v3: A_iarray_list$] : (v1 = v0 | % 74.23/10.90 ~ (nths$(v3, v2) = v1) | ~ (nths$(v3, v2) = v0)) & ! [v0: % 74.23/10.90 A_iarray_list_a_iarray_list_a_iarray_list_bool_fun_fun_fun$] : ! [v1: % 74.23/10.90 A_iarray_list_a_iarray_list_a_iarray_list_bool_fun_fun_fun$] : ! [v2: % 74.23/10.90 A_iarray_list$] : ! [v3: % 74.23/10.90 A_iarray_list_a_iarray_list_a_iarray_list_a_iarray_list_bool_fun_fun_fun_fun$] % 74.23/10.90 : (v1 = v0 | ~ (fun_app$bf(v3, v2) = v1) | ~ (fun_app$bf(v3, v2) = v0)) & ! % 74.23/10.90 [v0: A_iarray_list_a_iarray_list_bool_fun_fun$] : ! [v1: % 74.23/10.90 A_iarray_list_a_iarray_list_bool_fun_fun$] : ! [v2: A_iarray_list$] : ! % 74.23/10.90 [v3: A_iarray_list_a_iarray_list_a_iarray_list_bool_fun_fun_fun$] : (v1 = v0 | % 74.23/10.90 ~ (fun_app$be(v3, v2) = v1) | ~ (fun_app$be(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list$] : ! [v1: A_iarray_list_list$] : ! [v2: % 74.23/10.91 A_iarray_list_list$] : ! [v3: A_iarray_list_list$] : (v1 = v0 | ~ % 74.23/10.91 (append$c(v3, v2) = v1) | ~ (append$c(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list$] : ! [v1: A_iarray_iarray_list$] : ! [v2: % 74.23/10.91 A_iarray_iarray_list$] : ! [v3: A_iarray_iarray_list$] : (v1 = v0 | ~ % 74.23/10.91 (append$b(v3, v2) = v1) | ~ (append$b(v3, v2) = v0)) & ! [v0: Int_list$] : % 74.23/10.91 ! [v1: Int_list$] : ! [v2: Int_list$] : ! [v3: Int_list$] : (v1 = v0 | ~ % 74.23/10.91 (append$a(v3, v2) = v1) | ~ (append$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v1: Nat_a_iarray_prod_list$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v3: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$bd(v3, v2) = v1) | ~ (fun_app$bd(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: Nat$] : ! [v3: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : (v1 = v0 | ~ (lexn$b(v3, v2) = v1) | ~ % 74.23/10.91 (lexn$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v2: Nat$] : ! [v3: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (lexn$a(v3, v2) = v1) % 74.23/10.91 | ~ (lexn$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v2: Nat$] : % 74.23/10.91 ! [v3: Nat_a_iarray_prod_nat_a_iarray_prod_prod_set$] : (v1 = v0 | ~ % 74.23/10.91 (lexn$(v3, v2) = v1) | ~ (lexn$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_list_prod_list$] : ! [v1: Nat_a_iarray_list_prod_list$] : ! % 74.23/10.91 [v2: A_iarray_list_list$] : ! [v3: Nat$] : (v1 = v0 | ~ (enumerate$b(v3, v2) % 74.23/10.91 = v1) | ~ (enumerate$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_nat_a_iarray_prod_prod_list$] : ! [v1: % 74.23/10.91 Nat_nat_a_iarray_prod_prod_list$] : ! [v2: Nat_a_iarray_prod_list$] : ! % 74.23/10.91 [v3: Nat$] : (v1 = v0 | ~ (enumerate$a(v3, v2) = v1) | ~ (enumerate$a(v3, % 74.23/10.91 v2) = v0)) & ! [v0: A_iarray_list_set$] : ! [v1: A_iarray_list_set$] : % 74.23/10.91 ! [v2: A_iarray$] : ! [v3: A_iarray_list_set$] : (v1 = v0 | ~ (shift$(v3, % 74.23/10.91 v2) = v1) | ~ (shift$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod$] : ! [v1: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod$] : ! [v2: A_iarray_list_list$] % 74.23/10.91 : ! [v3: A_iarray_list_list$] : (v1 = v0 | ~ (pair$z(v3, v2) = v1) | ~ % 74.23/10.91 (pair$z(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod$] : (v1 = v0 | ~ (member$s(v3, % 74.23/10.91 v2) = v1) | ~ (member$s(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_nat_a_iarray_prod_prod$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_nat_a_iarray_prod_prod$] : ! [v2: Nat_a_iarray_prod$] : % 74.23/10.91 ! [v3: Nat_a_iarray_prod$] : (v1 = v0 | ~ (pair$y(v3, v2) = v1) | ~ % 74.23/10.91 (pair$y(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: Nat_a_iarray_prod_nat_a_iarray_prod_prod_set$] % 74.23/10.91 : ! [v3: Nat_a_iarray_prod_nat_a_iarray_prod_prod$] : (v1 = v0 | ~ % 74.23/10.91 (member$r(v3, v2) = v1) | ~ (member$r(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v3: Nat_a_iarray_prod_list$] : (v1 = v0 | ~ % 74.23/10.91 (pair$x(v3, v2) = v1) | ~ (pair$x(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v3: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod$] : (v1 = v0 | ~ % 74.23/10.91 (member$q(v3, v2) = v1) | ~ (member$q(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list$] : ! [v1: A_iarray_iarray_list$] : ! [v2: % 74.23/10.91 A_iarray_iarray_list$] : ! [v3: A_iarray_iarray$] : (v1 = v0 | ~ % 74.23/10.91 (cons$d(v3, v2) = v1) | ~ (cons$d(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray_list$] : ! [v3: A_iarray_iarray_list$] : (v1 = v0 | ~ % 74.23/10.91 (pair$w(v3, v2) = v1) | ~ (pair$w(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod$] : (v1 = v0 | ~ % 74.23/10.91 (member$p(v3, v2) = v1) | ~ (member$p(v3, v2) = v0)) & ! [v0: Int_list$] : % 74.23/10.91 ! [v1: Int_list$] : ! [v2: Int_list$] : ! [v3: int] : (v1 = v0 | ~ % 74.23/10.91 (cons$c(v3, v2) = v1) | ~ (cons$c(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_list_int_list_prod$] : ! [v1: Int_list_int_list_prod$] : ! [v2: % 74.23/10.91 Int_list$] : ! [v3: Int_list$] : (v1 = v0 | ~ (pair$v(v3, v2) = v1) | ~ % 74.23/10.91 (pair$v(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: Int_list_int_list_prod_set$] : ! [v3: % 74.23/10.91 Int_list_int_list_prod$] : (v1 = v0 | ~ (member$o(v3, v2) = v1) | ~ % 74.23/10.91 (member$o(v3, v2) = v0)) & ! [v0: Nat_a_iarray_prod$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod$] : ! [v2: A_iarray$] : ! [v3: Nat$] : (v1 = v0 | ~ % 74.23/10.91 (pair$u(v3, v2) = v1) | ~ (pair$u(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v1: Nat_a_iarray_prod_list$] : ! [v2: % 74.23/10.91 A_iarray_list$] : ! [v3: Nat$] : (v1 = v0 | ~ (enumerate$(v3, v2) = v1) | % 74.23/10.91 ~ (enumerate$(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 A_iarray$] : ! [v3: A_iarray_nat_fun$] : (v1 = v0 | ~ (fun_app$bc(v3, v2) % 74.23/10.91 = v1) | ~ (fun_app$bc(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 74.23/10.91 [v2: A_iarray_list$] : ! [v3: A_iarray_nat_fun$] : (v1 = v0 | ~ % 74.23/10.91 (size_list$(v3, v2) = v1) | ~ (size_list$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list$] : ! [v1: A_iarray_list_list$] : ! [v2: % 74.23/10.91 A_iarray_list_list$] : ! [v3: A_iarray_list$] : (v1 = v0 | ~ (cons$b(v3, % 74.23/10.91 v2) = v1) | ~ (cons$b(v3, v2) = v0)) & ! [v0: Nat_a_iarray_prod_list$] % 74.23/10.91 : ! [v1: Nat_a_iarray_prod_list$] : ! [v2: Nat_a_iarray_prod_list$] : ! % 74.23/10.91 [v3: Nat_a_iarray_prod$] : (v1 = v0 | ~ (cons$a(v3, v2) = v1) | ~ % 74.23/10.91 (cons$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod$] : ! [v1: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod$] : ! [v3: A_iarray_a_iarray_prod$] : (v1 = v0 | ~ % 74.23/10.91 (pair$t(v3, v2) = v1) | ~ (pair$t(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_a_iarray_prod_set_fun$] : ! [v3: A_iarray_bool_fun$] : % 74.23/10.91 (v1 = v0 | ~ (same_fst$c(v3, v2) = v1) | ~ (same_fst$c(v3, v2) = v0)) & ! % 74.23/10.91 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_a_iarray_prod_a_iarray_a_iarray_prod_prod$] : (v1 = v0 | ~ % 74.23/10.91 (member$n(v3, v2) = v1) | ~ (member$n(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : ! [v1: A_iarray_a_iarray_prod_set$] : ! % 74.23/10.91 [v2: A_iarray$] : ! [v3: A_iarray_a_iarray_a_iarray_prod_set_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$bb(v3, v2) = v1) | ~ (fun_app$bb(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod$] : % 74.23/10.91 ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod$] : % 74.23/10.91 ! [v2: A_iarray_list_a_iarray_list_prod$] : ! [v3: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : (v1 = v0 | ~ (pair$s(v3, v2) = v1) | % 74.23/10.91 ~ (pair$s(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod_set$] % 74.23/10.91 : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod_set$] % 74.23/10.91 : ! [v2: A_iarray_list_a_iarray_list_a_iarray_list_prod_set_fun$] : ! [v3: % 74.23/10.91 A_iarray_list_bool_fun$] : (v1 = v0 | ~ (same_fst$b(v3, v2) = v1) | ~ % 74.23/10.91 (same_fst$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod_set$] % 74.23/10.91 : ! [v3: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_a_iarray_list_a_iarray_list_prod_prod$] : % 74.23/10.91 (v1 = v0 | ~ (member$m(v3, v2) = v1) | ~ (member$m(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: A_iarray_list$] : ! [v3: % 74.23/10.91 A_iarray_list_a_iarray_list_a_iarray_list_prod_set_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$ba(v3, v2) = v1) | ~ (fun_app$ba(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod$] % 74.23/10.91 : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod$] % 74.23/10.91 : ! [v2: A_iarray_iarray_a_iarray_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : (v1 = v0 | ~ (pair$r(v3, v2) = v1) % 74.23/10.91 | ~ (pair$r(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod_set$] % 74.23/10.91 : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod_set$] % 74.23/10.91 : ! [v2: A_iarray_iarray_a_iarray_iarray_a_iarray_iarray_prod_set_fun$] : ! % 74.23/10.91 [v3: A_iarray_iarray_bool_fun$] : (v1 = v0 | ~ (same_fst$a(v3, v2) = v1) | ~ % 74.23/10.91 (same_fst$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod_set$] % 74.23/10.91 : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_prod$] % 74.23/10.91 : (v1 = v0 | ~ (member$l(v3, v2) = v1) | ~ (member$l(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v2: A_iarray_iarray$] : ! % 74.23/10.91 [v3: A_iarray_iarray_a_iarray_iarray_a_iarray_iarray_prod_set_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$az(v3, v2) = v1) | ~ (fun_app$az(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_prod_int_int_prod_prod_set$] : ! [v1: % 74.23/10.91 Int_int_prod_int_int_prod_prod_set$] : ! [v2: Int_int_int_prod_set_fun$] : % 74.23/10.91 ! [v3: Int_bool_fun$] : (v1 = v0 | ~ (same_fst$(v3, v2) = v1) | ~ % 74.23/10.91 (same_fst$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: Int_int_prod_int_int_prod_prod_set$] : ! [v3: % 74.23/10.91 Int_int_prod_int_int_prod_prod$] : (v1 = v0 | ~ (member$k(v3, v2) = v1) | % 74.23/10.91 ~ (member$k(v3, v2) = v0)) & ! [v0: Int_int_prod_set$] : ! [v1: % 74.23/10.91 Int_int_prod_set$] : ! [v2: int] : ! [v3: Int_int_int_prod_set_fun$] : (v1 % 74.23/10.91 = v0 | ~ (fun_app$ay(v3, v2) = v1) | ~ (fun_app$ay(v3, v2) = v0)) & ! % 74.23/10.91 [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_n_vec_n_vec_option$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_option_nat_fun$] : (v1 = v0 | ~ (fun_app$ax(v3, v2) = v1) | % 74.23/10.91 ~ (fun_app$ax(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_option_nat_fun$] : (v1 = % 74.23/10.91 v0 | ~ (fun_app$aw(v3, v2) = v1) | ~ (fun_app$aw(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_bool_fun_fun$] : ! [v1: Int_int_bool_fun_fun$] : ! [v2: % 74.23/10.91 Int_int_bool_fun_fun$] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (relcompp$b(v3, v2) = v1) | ~ (relcompp$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_prod_bool_fun$] : ! [v1: Int_int_prod_bool_fun$] : ! [v2: % 74.23/10.91 Int_int_bool_fun_fun$] : ! [v3: % 74.23/10.91 Int_int_bool_fun_fun_int_int_prod_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$av(v3, v2) = v1) | ~ (fun_app$av(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (relcompp$a(v3, v2) = v1) | ~ (relcompp$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_bool_fun$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_bool_fun$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun_a_iarray_iarray_a_iarray_iarray_prod_bool_fun_fun$] % 74.23/10.91 : (v1 = v0 | ~ (fun_app$au(v3, v2) = v1) | ~ (fun_app$au(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (relcompp$(v3, % 74.23/10.91 v2) = v1) | ~ (relcompp$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_bool_fun$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_bool_fun$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun_a_n_vec_n_vec_a_n_vec_n_vec_prod_bool_fun_fun$] % 74.23/10.91 : (v1 = v0 | ~ (fun_app$at(v3, v2) = v1) | ~ (fun_app$at(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : % 74.23/10.91 ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : ! % 74.23/10.91 [v2: A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (fstOp$b(v3, v2) % 74.23/10.91 = v1) | ~ (fstOp$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : ! % 74.23/10.91 [v1: A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_a_n_vec_n_vec_prod_fun$] : % 74.23/10.91 ! [v2: A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (sndOp$b(v3, v2) % 74.23/10.91 = v1) | ~ (sndOp$b(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 74.23/10.91 Nat_bool_fun$] : ! [v2: Nat$] : ! [v3: Nat_nat_bool_fun_fun$] : (v1 = v0 | % 74.23/10.91 ~ (fun_app$as(v3, v2) = v1) | ~ (fun_app$as(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_int_int_prod_prod$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_int_int_prod_prod$] : ! [v2: Int_int_prod$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec$] : (v1 = v0 | ~ (pair$q(v3, v2) = v1) | ~ (pair$q(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_n_vec_n_vec_int_prod$] : ! [v1: A_n_vec_n_vec_int_prod$] % 74.23/10.91 : ! [v2: int] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (pair$p(v3, v2) = v1) % 74.23/10.91 | ~ (pair$p(v3, v2) = v0)) & ! [v0: Int_int_prod_a_n_vec_n_vec_prod$] : ! % 74.23/10.91 [v1: Int_int_prod_a_n_vec_n_vec_prod$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 74.23/10.91 Int_int_prod$] : (v1 = v0 | ~ (pair$o(v3, v2) = v1) | ~ (pair$o(v3, v2) = % 74.23/10.91 v0)) & ! [v0: Int_int_prod_int_int_prod_prod$] : ! [v1: % 74.23/10.91 Int_int_prod_int_int_prod_prod$] : ! [v2: Int_int_prod$] : ! [v3: % 74.23/10.91 Int_int_prod$] : (v1 = v0 | ~ (pair$n(v3, v2) = v1) | ~ (pair$n(v3, v2) = % 74.23/10.91 v0)) & ! [v0: Int_a_n_vec_n_vec_prod$] : ! [v1: Int_a_n_vec_n_vec_prod$] % 74.23/10.91 : ! [v2: A_n_vec_n_vec$] : ! [v3: int] : (v1 = v0 | ~ (pair$m(v3, v2) = v1) % 74.23/10.91 | ~ (pair$m(v3, v2) = v0)) & ! [v0: A_n_vec_iarray$] : ! [v1: % 74.23/10.91 A_n_vec_iarray$] : ! [v2: A_n_vec_iarray$] : ! [v3: A_n_vec_iarray$] : (v1 % 74.23/10.91 = v0 | ~ (plus$x(v3, v2) = v1) | ~ (plus$x(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: Nat$] : ! [v3: % 74.23/10.91 Nat_a_iarray_list_fun$] : (v1 = v0 | ~ (fun_app$ar(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$ar(v3, v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: % 74.23/10.91 A_iarray_iarray$] : ! [v2: int] : ! [v3: Int_a_iarray_iarray_fun$] : (v1 = % 74.23/10.91 v0 | ~ (fun_app$aq(v3, v2) = v1) | ~ (fun_app$aq(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: Nat$] : ! [v3: % 74.23/10.91 Nat_a_iarray_iarray_fun$] : (v1 = v0 | ~ (fun_app$ap(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$ap(v3, v2) = v0)) & ! [v0: A_iarray$] : ! [v1: A_iarray$] : ! % 74.23/10.91 [v2: int] : ! [v3: Int_a_iarray_fun$] : (v1 = v0 | ~ (fun_app$ao(v3, v2) = % 74.23/10.91 v1) | ~ (fun_app$ao(v3, v2) = v0)) & ! [v0: A_iarray$] : ! [v1: % 74.23/10.91 A_iarray$] : ! [v2: Nat$] : ! [v3: Nat_a_iarray_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$an(v3, v2) = v1) | ~ (fun_app$an(v3, v2) = v0)) & ! [v0: int] : % 74.23/10.91 ! [v1: int] : ! [v2: A_iarray_list$] : ! [v3: A_iarray_list_int_fun$] : (v1 % 74.23/10.91 = v0 | ~ (fun_app$am(v3, v2) = v1) | ~ (fun_app$am(v3, v2) = v0)) & ! % 74.23/10.91 [v0: int] : ! [v1: int] : ! [v2: A_iarray$] : ! [v3: A_iarray_int_fun$] : % 74.23/10.91 (v1 = v0 | ~ (fun_app$al(v3, v2) = v1) | ~ (fun_app$al(v3, v2) = v0)) & ! % 74.23/10.91 [v0: Int_int_prod_int_int_prod_fun$] : ! [v1: Int_int_prod_int_int_prod_fun$] % 74.23/10.91 : ! [v2: Int_int_bool_fun_fun$] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | % 74.23/10.91 ~ (fstOp$a(v3, v2) = v1) | ~ (fstOp$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.91 : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.91 : ! [v2: A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ (fstOp$(v3, % 74.23/10.91 v2) = v1) | ~ (fstOp$(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 74.23/10.91 [v2: int] : ! [v3: Int_int_fun$] : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | % 74.23/10.91 ~ (fun_app$ak(v3, v2) = v0)) & ! [v0: Int_int_prod_int_int_prod_fun$] : ! % 74.23/10.91 [v1: Int_int_prod_int_int_prod_fun$] : ! [v2: Int_int_bool_fun_fun$] : ! % 74.23/10.91 [v3: Int_int_bool_fun_fun$] : (v1 = v0 | ~ (sndOp$a(v3, v2) = v1) | ~ % 74.23/10.91 (sndOp$a(v3, v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: Int_int_prod$] : % 74.23/10.91 ! [v2: Int_int_prod$] : ! [v3: Int_int_prod_int_int_prod_fun$] : (v1 = v0 | % 74.23/10.91 ~ (fun_app$aj(v3, v2) = v1) | ~ (fun_app$aj(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.91 : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.91 : ! [v2: A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ (sndOp$(v3, % 74.23/10.91 v2) = v1) | ~ (sndOp$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_a_iarray_iarray_prod_fun$] % 74.23/10.91 : (v1 = v0 | ~ (fun_app$ai(v3, v2) = v1) | ~ (fun_app$ai(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: Nat$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan_upt_k$(v3, v2) = v1) | ~ % 74.23/10.91 (gauss_Jordan_upt_k$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: Nat$] : ! [v3: A_n_vec_n_vec$] % 74.23/10.91 : (v1 = v0 | ~ (gauss_Jordan_upt_k_PA$(v3, v2) = v1) | ~ % 74.23/10.91 (gauss_Jordan_upt_k_PA$(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec_bool_fun$] : % 74.23/10.91 ! [v1: A_n_vec_n_vec_bool_fun$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ah(v3, % 74.23/10.91 v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 74.23/10.91 ! [v1: MultipleValueBool] : ! [v2: A_iarray_a_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_a_iarray_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) % 74.23/10.91 | ~ (fun_app$ag(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: A_iarray_iarray_a_iarray_iarray_prod$] : ! % 74.23/10.91 [v3: A_iarray_iarray_a_iarray_iarray_prod_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$af(v3, v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Int_int_prod$] : % 74.23/10.91 ! [v3: Int_int_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$ae(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$ae(v3, v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: % 74.23/10.91 A_iarray_iarray$] : ! [v2: A_iarray_iarray$] : ! [v3: A_iarray_iarray$] : % 74.23/10.91 (v1 = v0 | ~ (matrix_matrix_mult_iarray$(v3, v2) = v1) | ~ % 74.23/10.91 (matrix_matrix_mult_iarray$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec$] : (v1 = v0 | ~ (pair$l(v3, v2) = v1) | ~ (pair$l(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_iarray_int_set_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_int_set_prod$] : ! [v2: A_iarray_iarray_int_set_prod$] : ! % 74.23/10.91 [v3: A_iarray_iarray_int_set_prod$] : (v1 = v0 | ~ (plus$w(v3, v2) = v1) | ~ % 74.23/10.91 (plus$w(v3, v2) = v0)) & ! [v0: A_iarray_iarray_int_set_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_int_set_prod$] : ! [v2: Int_set$] : ! [v3: % 74.23/10.91 A_iarray_iarray$] : (v1 = v0 | ~ (pair$k(v3, v2) = v1) | ~ (pair$k(v3, v2) % 74.23/10.91 = v0)) & ! [v0: Int_int_prod_int_prod$] : ! [v1: Int_int_prod_int_prod$] % 74.23/10.91 : ! [v2: Int_int_prod_int_prod$] : ! [v3: Int_int_prod_int_prod$] : (v1 = v0 % 74.23/10.91 | ~ (plus$v(v3, v2) = v1) | ~ (plus$v(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_prod_int_prod$] : ! [v1: Int_int_prod_int_prod$] : ! [v2: int] : % 74.23/10.91 ! [v3: Int_int_prod$] : (v1 = v0 | ~ (pair$j(v3, v2) = v1) | ~ (pair$j(v3, % 74.23/10.91 v2) = v0)) & ! [v0: Int_set_int_set_prod$] : ! [v1: % 74.23/10.91 Int_set_int_set_prod$] : ! [v2: Int_set_int_set_prod$] : ! [v3: % 74.23/10.91 Int_set_int_set_prod$] : (v1 = v0 | ~ (plus$u(v3, v2) = v1) | ~ % 74.23/10.91 (plus$u(v3, v2) = v0)) & ! [v0: Int_set_int_set_prod$] : ! [v1: % 74.23/10.91 Int_set_int_set_prod$] : ! [v2: Int_set$] : ! [v3: Int_set$] : (v1 = v0 | % 74.23/10.91 ~ (pair$i(v3, v2) = v1) | ~ (pair$i(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_int_prod$] : ! [v1: A_iarray_iarray_int_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray_int_prod$] : ! [v3: A_iarray_iarray_int_prod$] : (v1 = v0 | % 74.23/10.91 ~ (plus$t(v3, v2) = v1) | ~ (plus$t(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_int_prod$] : ! [v1: A_iarray_iarray_int_prod$] : ! [v2: % 74.23/10.91 int] : ! [v3: A_iarray_iarray$] : (v1 = v0 | ~ (pair$h(v3, v2) = v1) | ~ % 74.23/10.91 (pair$h(v3, v2) = v0)) & ! [v0: Int_int_int_prod_prod$] : ! [v1: % 74.23/10.91 Int_int_int_prod_prod$] : ! [v2: Int_int_int_prod_prod$] : ! [v3: % 74.23/10.91 Int_int_int_prod_prod$] : (v1 = v0 | ~ (plus$s(v3, v2) = v1) | ~ % 74.23/10.91 (plus$s(v3, v2) = v0)) & ! [v0: Int_int_int_prod_prod$] : ! [v1: % 74.23/10.91 Int_int_int_prod_prod$] : ! [v2: Int_int_prod$] : ! [v3: int] : (v1 = v0 | % 74.23/10.91 ~ (pair$g(v3, v2) = v1) | ~ (pair$g(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_a_iarray_iarray_prod$] : ! [v1: Int_a_iarray_iarray_prod$] : ! [v2: % 74.23/10.91 Int_a_iarray_iarray_prod$] : ! [v3: Int_a_iarray_iarray_prod$] : (v1 = v0 | % 74.23/10.91 ~ (plus$r(v3, v2) = v1) | ~ (plus$r(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_a_iarray_iarray_prod$] : ! [v1: Int_a_iarray_iarray_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray$] : ! [v3: int] : (v1 = v0 | ~ (pair$f(v3, v2) = v1) | ~ % 74.23/10.91 (pair$f(v3, v2) = v0)) & ! [v0: A_iarray_a_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_a_iarray_prod$] : ! [v2: A_iarray_a_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_a_iarray_prod$] : (v1 = v0 | ~ (plus$q(v3, v2) = v1) | ~ % 74.23/10.91 (plus$q(v3, v2) = v0)) & ! [v0: Int_set_int_prod$] : ! [v1: % 74.23/10.91 Int_set_int_prod$] : ! [v2: Int_set_int_prod$] : ! [v3: Int_set_int_prod$] % 74.23/10.91 : (v1 = v0 | ~ (plus$p(v3, v2) = v1) | ~ (plus$p(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_set_int_prod$] : ! [v1: Int_set_int_prod$] : ! [v2: int] : ! [v3: % 74.23/10.91 Int_set$] : (v1 = v0 | ~ (pair$e(v3, v2) = v1) | ~ (pair$e(v3, v2) = v0)) % 74.23/10.91 & ! [v0: Int_int_set_prod$] : ! [v1: Int_int_set_prod$] : ! [v2: % 74.23/10.91 Int_int_set_prod$] : ! [v3: Int_int_set_prod$] : (v1 = v0 | ~ (plus$o(v3, % 74.23/10.91 v2) = v1) | ~ (plus$o(v3, v2) = v0)) & ! [v0: Int_int_set_prod$] : ! % 74.23/10.91 [v1: Int_int_set_prod$] : ! [v2: Int_set$] : ! [v3: int] : (v1 = v0 | ~ % 74.23/10.91 (pair$d(v3, v2) = v1) | ~ (pair$d(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] % 74.23/10.91 : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] % 74.23/10.91 : (v1 = v0 | ~ (matrix_matrix_mult$(v3, v2) = v1) | ~ % 74.23/10.91 (matrix_matrix_mult$(v3, v2) = v0)) & ! [v0: A_iarray_list$] : ! [v1: % 74.23/10.91 A_iarray_list$] : ! [v2: A_iarray_list$] : ! [v3: A_iarray_list$] : (v1 = % 74.23/10.91 v0 | ~ (splice$b(v3, v2) = v1) | ~ (splice$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list$] : ! [v1: A_iarray_list_list$] : ! [v2: % 74.23/10.91 A_iarray_list_list$] : ! [v3: A_iarray_list_list$] : (v1 = v0 | ~ % 74.23/10.91 (splice$a(v3, v2) = v1) | ~ (splice$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v1: Nat_a_iarray_prod_list$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v3: Nat_a_iarray_prod_list$] : (v1 = v0 | ~ % 74.23/10.91 (splice$(v3, v2) = v1) | ~ (splice$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_prod_set$] : ! [v1: Int_int_prod_set$] : ! [v2: Int_int_prod_set$] % 74.23/10.91 : ! [v3: Int_int_prod_set$] : (v1 = v0 | ~ (plus$n(v3, v2) = v1) | ~ % 74.23/10.91 (plus$n(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec_set$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_set$] : ! [v2: A_n_vec_n_vec_set$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_set$] : (v1 = v0 | ~ (plus$m(v3, v2) = v1) | ~ (plus$m(v3, % 74.23/10.91 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 74.23/10.91 ! [v2: A_n_vec_n_vec_set$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 74.23/10.91 (member$j(v3, v2) = v1) | ~ (member$j(v3, v2) = v0)) & ! [v0: Int_set$] : % 74.23/10.91 ! [v1: Int_set$] : ! [v2: Int_set$] : ! [v3: Int_set$] : (v1 = v0 | ~ % 74.23/10.91 (plus$k(v3, v2) = v1) | ~ (plus$k(v3, v2) = v0)) & ! [v0: Int_set_set$] : % 74.23/10.91 ! [v1: Int_set_set$] : ! [v2: Int_set_set$] : ! [v3: Int_set_set$] : (v1 = % 74.23/10.91 v0 | ~ (plus$l(v3, v2) = v1) | ~ (plus$l(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Int_set_set$] : ! % 74.23/10.91 [v3: Int_set$] : (v1 = v0 | ~ (member$i(v3, v2) = v1) | ~ (member$i(v3, v2) % 74.23/10.91 = v0)) & ! [v0: A_iarray_iarray_set$] : ! [v1: A_iarray_iarray_set$] : % 74.23/10.91 ! [v2: A_iarray_iarray_set$] : ! [v3: A_iarray_iarray_set$] : (v1 = v0 | ~ % 74.23/10.91 (plus$j(v3, v2) = v1) | ~ (plus$j(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_iarray_set$] : ! [v3: A_iarray_iarray$] : (v1 = v0 | ~ % 74.23/10.91 (member$h(v3, v2) = v1) | ~ (member$h(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (plus$i(v3, v2) = % 74.23/10.91 v1) | ~ (plus$i(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 Nat$] : ! [v3: Nat$] : (v1 = v0 | ~ (plus$g(v3, v2) = v1) | ~ (plus$g(v3, % 74.23/10.91 v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_set$] : % 74.23/10.91 ! [v3: Nat_set$] : (v1 = v0 | ~ (plus$h(v3, v2) = v1) | ~ (plus$h(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray$] : ! [v1: A_iarray$] : ! [v2: A_iarray$] : ! % 74.23/10.91 [v3: A_iarray_a_iarray_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$ad(v3, v2) = v0)) & ! [v0: A_iarray_set$] : ! [v1: A_iarray_set$] % 74.23/10.91 : ! [v2: A_iarray_set$] : ! [v3: A_iarray_set$] : (v1 = v0 | ~ (plus$f(v3, % 74.23/10.91 v2) = v1) | ~ (plus$f(v3, v2) = v0)) & ! [v0: A_iarray_iarray$] : ! % 74.23/10.91 [v1: A_iarray_iarray$] : ! [v2: A_iarray_iarray$] : ! [v3: A_iarray_iarray$] % 74.23/10.91 : (v1 = v0 | ~ (plus$d(v3, v2) = v1) | ~ (plus$d(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : (v1 = v0 | ~ (plus$c(v3, v2) = v1) % 74.23/10.91 | ~ (plus$c(v3, v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: % 74.23/10.91 Int_int_prod$] : ! [v2: Int_int_prod$] : ! [v3: Int_int_prod$] : (v1 = v0 % 74.23/10.91 | ~ (plus$b(v3, v2) = v1) | ~ (plus$b(v3, v2) = v0)) & ! [v0: int] : ! % 74.23/10.91 [v1: int] : ! [v2: Int_int_prod$] : ! [v3: Int_int_prod_int_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! % 74.23/10.91 [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (plus$a(v3, v2) = v1) | ~ (plus$a(v3, % 74.23/10.91 v2) = v0)) & ! [v0: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : (v1 = v0 | ~ (plus$(v3, v2) = v1) | ~ % 74.23/10.91 (plus$(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : % 74.23/10.91 ! [v2: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_a_n_vec_n_vec_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$ab(v3, v2) = v1) | ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: tlbool] % 74.23/10.91 : ! [v1: tlbool] : ! [v2: A_iarray_iarray_option$] : ! [v3: % 74.23/10.91 A_iarray_iarray_bool_fun$] : (v1 = v0 | ~ (def_7(v3, v2) = v1) | ~ % 74.23/10.91 (def_7(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 74.23/10.91 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_bool_fun$] : (v1 = v0 | % 74.23/10.91 ~ (def_5(v3, v2) = v1) | ~ (def_5(v3, v2) = v0)) & ! [v0: tlbool] : ! % 74.23/10.91 [v1: tlbool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (def_3(v3, v2) = v1) | ~ (def_3(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list$] : ! [v1: A_iarray_list_list$] : ! [v2: % 74.23/10.91 A_iarray_list_list$] : ! [v3: A_iarray_list_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (filter$b(v3, v2) = v1) | ~ (filter$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v1: Nat_a_iarray_prod_list$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v3: Nat_a_iarray_prod_bool_fun$] : (v1 = v0 | % 74.23/10.91 ~ (filter$a(v3, v2) = v1) | ~ (filter$a(v3, v2) = v0)) & ! [v0: Nat$] : % 74.23/10.91 ! [v1: Nat$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec_nat_fun$] : (v1 % 74.23/10.91 = v0 | ~ (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_iarray_option_bool_fun$] : ! [v1: % 74.23/10.91 A_iarray_iarray_option_bool_fun$] : ! [v2: A_iarray_iarray_bool_fun$] : ! % 74.23/10.91 [v3: tlbool] : (v1 = v0 | ~ (case_option$a(v3, v2) = v1) | ~ % 74.23/10.91 (case_option$a(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec_option_bool_fun$] : ! % 74.23/10.91 [v1: A_n_vec_n_vec_option_bool_fun$] : ! [v2: A_n_vec_n_vec_bool_fun$] : ! % 74.23/10.91 [v3: tlbool] : (v1 = v0 | ~ (case_option$(v3, v2) = v1) | ~ % 74.23/10.91 (case_option$(v3, v2) = v0)) & ! [v0: A_iarray_iarray_option_bool_fun$] : % 74.23/10.91 ! [v1: A_iarray_iarray_option_bool_fun$] : ! [v2: A_iarray_iarray_option$] : % 74.23/10.91 ! [v3: A_iarray_iarray_option_a_iarray_iarray_option_bool_fun_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$z(v3, v2) = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_option_bool_fun$] : ! [v1: A_n_vec_n_vec_option_bool_fun$] : % 74.23/10.91 ! [v2: A_iarray_iarray_option$] : ! [v3: % 74.23/10.91 A_iarray_iarray_option_a_n_vec_n_vec_option_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$y(v3, v2) = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_option_bool_fun$] : ! [v1: % 74.23/10.91 A_iarray_iarray_option_bool_fun$] : ! [v2: A_n_vec_n_vec_option$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_option_a_iarray_iarray_option_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$x(v3, v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_option_bool_fun$] : ! [v1: A_n_vec_n_vec_option_bool_fun$] : % 74.23/10.91 ! [v2: A_n_vec_n_vec_option$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_option_a_n_vec_n_vec_option_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$w(v3, v2) = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: Nat$] : ! % 74.23/10.91 [v1: Nat$] : ! [v2: A_iarray_list_list$] : ! [v3: % 74.23/10.91 A_iarray_list_list_nat_fun$] : (v1 = v0 | ~ (fun_app$v(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$v(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : ! [v3: Nat_a_iarray_prod_list_nat_fun$] : (v1 = % 74.23/10.91 v0 | ~ (fun_app$u(v3, v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_iarray_option$] : ! [v3: A_iarray_iarray_option_bool_fun$] : (v1 = % 74.23/10.91 v0 | ~ (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_option$] : ! [v3: A_n_vec_n_vec_option_bool_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_a_iarray_iarray_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: Nat$] : ! % 74.23/10.91 [v1: Nat$] : ! [v2: A_iarray_iarray$] : ! [v3: A_iarray_iarray_nat_fun$] : % 74.23/10.91 (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ (fun_app$q(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: A_iarray_list$] : ! % 74.23/10.91 [v3: A_iarray_list_a_iarray_list_fun$] : (v1 = v0 | ~ (fun_app$p(v3, v2) = % 74.23/10.91 v1) | ~ (fun_app$p(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 74.23/10.91 A_n_vec_n_vec_bool_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 74.23/10.91 (fun_app$o(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 74.23/10.91 A_iarray_iarray$] : ! [v3: A_iarray_iarray_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (def_1(v3, v2) = v1) | ~ (def_1(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 74.23/10.91 : ! [v1: MultipleValueBool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : (v1 % 74.23/10.91 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_bool_fun$] : ! [v1: A_iarray_iarray_bool_fun$] : ! [v2: % 74.23/10.91 A_iarray_iarray_bool_fun$] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (uue$(v3, v2) = v1) | ~ (uue$(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: % 74.23/10.91 Nat$] : ! [v2: A_iarray_list$] : ! [v3: A_iarray_list_nat_fun$] : (v1 = v0 % 74.23/10.91 | ~ (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: int] % 74.23/10.91 : ! [v1: int] : ! [v2: Nat$] : ! [v3: Nat_int_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: Nat$] : ! % 74.23/10.91 [v1: Nat$] : ! [v2: int] : ! [v3: Int_nat_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: % 74.23/10.91 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : ! [v3: % 74.23/10.91 A_iarray_list$] : (v1 = v0 | ~ (uut$(v3, v2) = v1) | ~ (uut$(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_bool_fun$] : ! [v1: A_iarray_bool_fun$] : ! [v2: % 74.23/10.91 A_iarray_bool_fun$] : ! [v3: A_iarray_bool_fun$] : (v1 = v0 | ~ (uua$(v3, % 74.23/10.91 v2) = v1) | ~ (uua$(v3, v2) = v0)) & ! [v0: A_iarray_list_bool_fun$] : % 74.23/10.91 ! [v1: A_iarray_list_bool_fun$] : ! [v2: A_iarray$] : ! [v3: % 74.23/10.91 A_iarray_list_set$] : (v1 = v0 | ~ (uus$(v3, v2) = v1) | ~ (uus$(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: % 74.23/10.91 A_iarray_list$] : ! [v3: A_iarray$] : (v1 = v0 | ~ (cons$(v3, v2) = v1) | % 74.23/10.91 ~ (cons$(v3, v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: Int_bool_fun$] : % 74.23/10.91 ! [v2: int] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$j(v3, % 74.23/10.91 v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! [v0: Int_int_prod$] : ! % 74.23/10.91 [v1: Int_int_prod$] : ! [v2: int] : ! [v3: int] : (v1 = v0 | ~ (pair$c(v3, % 74.23/10.91 v2) = v1) | ~ (pair$c(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 74.23/10.91 [v1: MultipleValueBool] : ! [v2: Int_int_prod_set$] : ! [v3: Int_int_prod$] % 74.23/10.91 : (v1 = v0 | ~ (member$g(v3, v2) = v1) | ~ (member$g(v3, v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_list_bool_fun$] : ! [v1: A_iarray_list_bool_fun$] : ! [v2: % 74.23/10.91 A_iarray_list$] : ! [v3: A_iarray_list_a_iarray_list_bool_fun_fun$] : (v1 = % 74.23/10.91 v0 | ~ (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : ! [v2: A_iarray_list$] : ! [v3: % 74.23/10.91 A_iarray_list$] : (v1 = v0 | ~ (pair$b(v3, v2) = v1) | ~ (pair$b(v3, v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_bool_fun$] : ! [v1: A_iarray_bool_fun$] : ! [v2: % 74.23/10.91 A_iarray$] : ! [v3: A_iarray_a_iarray_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$h(v3, v2) = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_a_iarray_prod$] : ! [v1: A_iarray_a_iarray_prod$] : ! [v2: % 74.23/10.91 A_iarray$] : ! [v3: A_iarray$] : (v1 = v0 | ~ (pair$a(v3, v2) = v1) | ~ % 74.23/10.91 (pair$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: A_iarray_a_iarray_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_a_iarray_prod$] : (v1 = v0 | ~ (member$f(v3, v2) = v1) | ~ % 74.23/10.91 (member$f(v3, v2) = v0)) & ! [v0: A_iarray_iarray_bool_fun$] : ! [v1: % 74.23/10.91 A_iarray_iarray_bool_fun$] : ! [v2: A_iarray_iarray$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_iarray_iarray$] % 74.23/10.91 : ! [v3: A_iarray_iarray_bool_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) % 74.23/10.91 | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v2: A_iarray_iarray$] : ! [v3: % 74.23/10.91 A_iarray_iarray$] : (v1 = v0 | ~ (pair$(v3, v2) = v1) | ~ (pair$(v3, v2) = % 74.23/10.91 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v3: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : (v1 = v0 | ~ (member$e(v3, v2) = % 74.23/10.91 v1) | ~ (member$e(v3, v2) = v0)) & ! [v0: A_iarray_bool_fun$] : ! [v1: % 74.23/10.91 A_iarray_bool_fun$] : ! [v2: A_iarray_list$] : ! [v3: A_iarray_bool_fun$] % 74.23/10.91 : (v1 = v0 | ~ (uuu$(v3, v2) = v1) | ~ (uuu$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod$] : ! [v3: Nat_a_iarray_prod_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 74.23/10.91 Int_bool_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, % 74.23/10.91 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 74.23/10.91 ! [v2: Int_set$] : ! [v3: int] : (v1 = v0 | ~ (member$d(v3, v2) = v1) | ~ % 74.23/10.91 (member$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! % 74.23/10.91 [v3: Nat$] : (v1 = v0 | ~ (member$c(v3, v2) = v1) | ~ (member$c(v3, v2) = % 74.23/10.91 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_list$] : ! [v3: A_iarray_list_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_list_set$] : ! [v3: A_iarray_list$] : (v1 = v0 | ~ (member$b(v3, % 74.23/10.91 v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 74.23/10.91 ! [v1: MultipleValueBool] : ! [v2: A_iarray_set$] : ! [v3: A_iarray$] : (v1 % 74.23/10.91 = v0 | ~ (member$a(v3, v2) = v1) | ~ (member$a(v3, v2) = v0)) & ! [v0: % 74.23/10.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : ! [v3: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$a(v3, % 74.23/10.91 v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 74.23/10.91 ! [v1: MultipleValueBool] : ! [v2: A_iarray_list_a_iarray_list_prod_set$] : % 74.23/10.91 ! [v3: A_iarray_list_a_iarray_list_prod$] : (v1 = v0 | ~ (member$(v3, v2) = % 74.23/10.91 v1) | ~ (member$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 74.23/10.91 MultipleValueBool] : ! [v2: A_iarray$] : ! [v3: A_iarray_bool_fun$] : (v1 % 74.23/10.91 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : (v1 = v0 | ~ (lenlex$(v2) = v1) | ~ % 74.23/10.91 (lenlex$(v2) = v0)) & ! [v0: A_iarray_list_list$] : ! [v1: % 74.23/10.91 A_iarray_list_list$] : ! [v2: A_iarray_list_list$] : (v1 = v0 | ~ % 74.23/10.91 (product_lists$(v2) = v1) | ~ (product_lists$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_set$] : ! [v1: A_iarray_list_set$] : ! [v2: % 74.23/10.91 A_iarray_list_list$] : (v1 = v0 | ~ (set$a(v2) = v1) | ~ (set$a(v2) = v0)) % 74.23/10.91 & ! [v0: A_iarray_list_a_iarray_list_fun$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_fun$] : ! [v2: A_iarray_list$] : (v1 = v0 | ~ % 74.23/10.91 (append$d(v2) = v1) | ~ (append$d(v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_fun$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_fun$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_list$] : (v1 = v0 | ~ (append$(v2) = v1) | ~ % 74.23/10.91 (append$(v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_nat_a_iarray_prod_prod_set$] : (v1 = v0 | ~ (lexord$d(v2) % 74.23/10.91 = v1) | ~ (lexord$d(v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_nat_a_iarray_prod_prod_set$] : (v1 = v0 | ~ % 74.23/10.91 (listrel1$d(v2) = v1) | ~ (listrel1$d(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : (v1 = v0 | ~ (listrel1$c(v2) = v1) | ~ % 74.23/10.91 (listrel1$c(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (listrel1$b(v2) = v1) % 74.23/10.91 | ~ (listrel1$b(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (listrel1$a(v2) = % 74.23/10.91 v1) | ~ (listrel1$a(v2) = v0)) & ! [v0: Int_list_int_list_prod_set$] : % 74.23/10.91 ! [v1: Int_list_int_list_prod_set$] : ! [v2: Int_int_prod_set$] : (v1 = v0 | % 74.23/10.91 ~ (listrel1$(v2) = v1) | ~ (listrel1$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : (v1 = v0 | ~ (lexord$c(v2) = v1) | ~ % 74.23/10.91 (lexord$c(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (lexord$b(v2) = v1) | % 74.23/10.91 ~ (lexord$b(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (lexord$a(v2) = % 74.23/10.91 v1) | ~ (lexord$a(v2) = v0)) & ! [v0: Int_list_int_list_prod_set$] : ! % 74.23/10.91 [v1: Int_list_int_list_prod_set$] : ! [v2: Int_int_prod_set$] : (v1 = v0 | ~ % 74.23/10.91 (lexord$(v2) = v1) | ~ (lexord$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] % 74.23/10.91 : ! [v2: Nat_a_iarray_list_prod_list$] : (v1 = v0 | ~ (size$h(v2) = v1) | ~ % 74.23/10.91 (size$h(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 Nat_nat_a_iarray_prod_prod_list$] : (v1 = v0 | ~ (size$g(v2) = v1) | ~ % 74.23/10.91 (size$g(v2) = v0)) & ! [v0: A_iarray_list_a_iarray_list_prod_set$] : ! % 74.23/10.91 [v1: A_iarray_list_a_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod_set$] : (v1 = v0 | ~ (lex$d(v2) = v1) | ~ % 74.23/10.91 (lex$d(v2) = v0)) & ! [v0: A_iarray_list_list_a_iarray_list_list_prod_set$] % 74.23/10.91 : ! [v1: A_iarray_list_list_a_iarray_list_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (lex$c(v2) = v1) | ~ % 74.23/10.91 (lex$c(v2) = v0)) & ! [v0: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_a_iarray_prod_list_prod_set$] : ! [v2: % 74.23/10.91 Nat_a_iarray_prod_nat_a_iarray_prod_prod_set$] : (v1 = v0 | ~ (lex$b(v2) = % 74.23/10.91 v1) | ~ (lex$b(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_iarray_list_a_iarray_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (lex$a(v2) = v1) % 74.23/10.91 | ~ (lex$a(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 A_iarray_iarray_list$] : (v1 = v0 | ~ (size$f(v2) = v1) | ~ (size$f(v2) = % 74.23/10.91 v0)) & ! [v0: Int_list_int_list_prod_set$] : ! [v1: % 74.23/10.91 Int_list_int_list_prod_set$] : ! [v2: Int_int_prod_set$] : (v1 = v0 | ~ % 74.23/10.91 (lex$(v2) = v1) | ~ (lex$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 74.23/10.91 [v2: Int_list$] : (v1 = v0 | ~ (size$e(v2) = v1) | ~ (size$e(v2) = v0)) & ! % 74.23/10.91 [v0: A_n_vec_n_vec_option_nat_fun$] : ! [v1: A_n_vec_n_vec_option_nat_fun$] : % 74.23/10.91 ! [v2: A_n_vec_n_vec_nat_fun$] : (v1 = v0 | ~ (size_option$a(v2) = v1) | ~ % 74.23/10.91 (size_option$a(v2) = v0)) & ! [v0: A_iarray_iarray_option_nat_fun$] : ! % 74.23/10.91 [v1: A_iarray_iarray_option_nat_fun$] : ! [v2: A_iarray_iarray_nat_fun$] : % 74.23/10.91 (v1 = v0 | ~ (size_option$(v2) = v1) | ~ (size_option$(v2) = v0)) & ! [v0: % 74.23/10.91 Int_int_prod_set$] : ! [v1: Int_int_prod_set$] : ! [v2: % 74.23/10.91 Int_int_prod_bool_fun$] : (v1 = v0 | ~ (collect$g(v2) = v1) | ~ % 74.23/10.91 (collect$g(v2) = v0)) & ! [v0: A_iarray_iarray_a_iarray_iarray_prod_set$] : % 74.23/10.91 ! [v1: A_iarray_iarray_a_iarray_iarray_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (collect$f(v2) = v1) | ~ (collect$f(v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_set$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_set$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod_bool_fun$] : (v1 = v0 | ~ (collect$e(v2) = % 74.23/10.91 v1) | ~ (collect$e(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_option$] : (v1 = v0 | ~ (size$d(v2) = v1) | ~ (size$d(v2) = % 74.23/10.91 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.23/10.91 A_n_vec_iarray$] : (v1 = v0 | ~ (is_zero_iarray$a(v2) = v1) | ~ % 74.23/10.91 (is_zero_iarray$a(v2) = v0)) & ! [v0: A_n_vec_iarray$] : ! [v1: % 74.23/10.91 A_n_vec_iarray$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ % 74.23/10.91 (vec_to_iarray$(v2) = v1) | ~ (vec_to_iarray$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v2: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : (v1 = v0 | ~ (swap$d(v2) = v1) | % 74.23/10.91 ~ (swap$d(v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: Int_int_prod$] : ! % 74.23/10.91 [v2: Int_int_prod$] : (v1 = v0 | ~ (swap$c(v2) = v1) | ~ (swap$c(v2) = v0)) % 74.23/10.91 & ! [v0: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec_a_n_vec_n_vec_prod$] : (v1 = v0 | ~ (swap$b(v2) = v1) | ~ % 74.23/10.91 (swap$b(v2) = v0)) & ! [v0: A_iarray_a_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_a_iarray_prod$] : ! [v2: A_iarray_a_iarray_prod$] : (v1 = v0 | ~ % 74.23/10.91 (swap$a(v2) = v1) | ~ (swap$a(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod$] : (v1 = v0 | ~ (swap$(v2) = v1) | ~ % 74.23/10.91 (swap$(v2) = v0)) & ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! % 74.23/10.91 [v2: A_iarray_list_a_iarray_list_prod$] : (v1 = v0 | ~ (fst$k(v2) = v1) | ~ % 74.23/10.91 (fst$k(v2) = v0)) & ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! % 74.23/10.91 [v2: A_iarray_list_a_iarray_list_prod$] : (v1 = v0 | ~ (snd$k(v2) = v1) | ~ % 74.23/10.91 (snd$k(v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: Int_int_prod$] : ! % 74.23/10.91 [v2: Int_int_prod_int_prod$] : (v1 = v0 | ~ (fst$j(v2) = v1) | ~ (fst$j(v2) % 74.23/10.91 = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Int_int_prod_int_prod$] : % 74.23/10.91 (v1 = v0 | ~ (snd$j(v2) = v1) | ~ (snd$j(v2) = v0)) & ! [v0: Int_set$] : ! % 74.23/10.91 [v1: Int_set$] : ! [v2: Int_set_int_set_prod$] : (v1 = v0 | ~ (fst$i(v2) = % 74.23/10.91 v1) | ~ (fst$i(v2) = v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! % 74.23/10.91 [v2: Int_set_int_set_prod$] : (v1 = v0 | ~ (snd$i(v2) = v1) | ~ (snd$i(v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 74.23/10.91 A_iarray_iarray_int_prod$] : (v1 = v0 | ~ (fst$h(v2) = v1) | ~ (fst$h(v2) % 74.23/10.91 = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: A_iarray_iarray_int_prod$] % 74.23/10.91 : (v1 = v0 | ~ (snd$h(v2) = v1) | ~ (snd$h(v2) = v0)) & ! [v0: int] : ! % 74.23/10.91 [v1: int] : ! [v2: Int_int_int_prod_prod$] : (v1 = v0 | ~ (fst$g(v2) = v1) | % 74.23/10.91 ~ (fst$g(v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: Int_int_prod$] : ! % 74.23/10.91 [v2: Int_int_int_prod_prod$] : (v1 = v0 | ~ (snd$g(v2) = v1) | ~ (snd$g(v2) % 74.23/10.91 = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Int_a_iarray_iarray_prod$] % 74.23/10.91 : (v1 = v0 | ~ (fst$f(v2) = v1) | ~ (fst$f(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 74.23/10.91 Int_a_iarray_iarray_prod$] : (v1 = v0 | ~ (snd$f(v2) = v1) | ~ (snd$f(v2) % 74.23/10.91 = v0)) & ! [v0: A_iarray$] : ! [v1: A_iarray$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod$] : (v1 = v0 | ~ (fst$e(v2) = v1) | ~ (fst$e(v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray$] : ! [v1: A_iarray$] : ! [v2: % 74.23/10.91 A_iarray_a_iarray_prod$] : (v1 = v0 | ~ (snd$e(v2) = v1) | ~ (snd$e(v2) = % 74.23/10.91 v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: Int_set_int_prod$] % 74.23/10.91 : (v1 = v0 | ~ (fst$d(v2) = v1) | ~ (fst$d(v2) = v0)) & ! [v0: int] : ! % 74.23/10.91 [v1: int] : ! [v2: Int_set_int_prod$] : (v1 = v0 | ~ (snd$d(v2) = v1) | ~ % 74.23/10.91 (snd$d(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Int_int_set_prod$] % 74.23/10.91 : (v1 = v0 | ~ (fst$c(v2) = v1) | ~ (fst$c(v2) = v0)) & ! [v0: Int_set$] : % 74.23/10.91 ! [v1: Int_set$] : ! [v2: Int_int_set_prod$] : (v1 = v0 | ~ (snd$c(v2) = v1) % 74.23/10.91 | ~ (snd$c(v2) = v0)) & ! [v0: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! % 74.23/10.91 [v1: A_n_vec_n_vec_a_n_vec_n_vec_prod$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | % 74.23/10.91 ~ (gauss_Jordan_PA$(v2) = v1) | ~ (gauss_Jordan_PA$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_nat_fun$] : ! [v1: A_iarray_list_nat_fun$] : ! [v2: Nat$] : % 74.23/10.91 (v1 = v0 | ~ (gen_length$b(v2) = v1) | ~ (gen_length$b(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_list_nat_fun$] : ! [v1: A_iarray_list_list_nat_fun$] : ! % 74.23/10.91 [v2: Nat$] : (v1 = v0 | ~ (gen_length$a(v2) = v1) | ~ (gen_length$a(v2) = % 74.23/10.91 v0)) & ! [v0: Nat_a_iarray_prod_list_nat_fun$] : ! [v1: % 74.23/10.91 Nat_a_iarray_prod_list_nat_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ % 74.23/10.91 (gen_length$(v2) = v1) | ~ (gen_length$(v2) = v0)) & ! [v0: Nat_bool_fun$] % 74.23/10.91 : ! [v1: Nat_bool_fun$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ % 74.23/10.91 (id_upt_k$(v2) = v1) | ~ (id_upt_k$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : % 74.23/10.91 ! [v1: A_n_vec_n_vec$] : ! [v2: A_iarray_iarray$] : (v1 = v0 | ~ % 74.23/10.91 (iarray_to_matrix$(v2) = v1) | ~ (iarray_to_matrix$(v2) = v0)) & ! [v0: % 74.23/10.91 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v1 = % 74.23/10.91 v0 | ~ (p_Gauss_Jordan$(v2) = v1) | ~ (p_Gauss_Jordan$(v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_a_iarray_fun$] : ! [v1: A_iarray_a_iarray_fun$] : ! [v2: % 74.23/10.91 A_iarray$] : (v1 = v0 | ~ (plus$e(v2) = v1) | ~ (plus$e(v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_set$] : ! [v1: A_iarray_set$] : ! [v2: A_iarray_bool_fun$] : % 74.23/10.91 (v1 = v0 | ~ (collect$d(v2) = v1) | ~ (collect$d(v2) = v0)) & ! [v0: % 74.23/10.91 Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (collect$c(v2) = v1) | ~ (collect$c(v2) = v0)) & ! [v0: Int_set$] : ! % 74.23/10.91 [v1: Int_set$] : ! [v2: Int_bool_fun$] : (v1 = v0 | ~ (collect$b(v2) = v1) | % 74.23/10.91 ~ (collect$b(v2) = v0)) & ! [v0: A_iarray_list_set$] : ! [v1: % 74.23/10.91 A_iarray_list_set$] : ! [v2: A_iarray_list_bool_fun$] : (v1 = v0 | ~ % 74.23/10.91 (collect$a(v2) = v1) | ~ (collect$a(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_set$] : ! [v2: % 74.23/10.91 A_iarray_list_a_iarray_list_prod_bool_fun$] : (v1 = v0 | ~ (collect$(v2) = % 74.23/10.91 v1) | ~ (collect$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_inv$(v2) = % 74.23/10.91 v1) | ~ (matrix_inv$(v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: % 74.23/10.91 A_iarray_iarray$] : ! [v2: A_iarray_iarray_option$] : (v1 = v0 | ~ % 74.23/10.91 (the$a(v2) = v1) | ~ (the$a(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 74.23/10.91 [v2: A_iarray_iarray_option$] : (v1 = v0 | ~ (size$c(v2) = v1) | ~ % 74.23/10.91 (size$c(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! % 74.23/10.91 [v2: A_n_vec_n_vec_option$] : (v1 = v0 | ~ (the$(v2) = v1) | ~ (the$(v2) = % 74.23/10.91 v0)) & ! [v0: A_n_vec_n_vec_option$] : ! [v1: A_n_vec_n_vec_option$] : % 74.23/10.91 ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (inverse_matrix$(v2) = v1) | ~ % 74.23/10.91 (inverse_matrix$(v2) = v0)) & ! [v0: A_iarray_iarray_option$] : ! [v1: % 74.23/10.91 A_iarray_iarray_option$] : ! [v2: A_n_vec_n_vec_option$] : (v1 = v0 | ~ % 74.23/10.91 (matrix_to_iarray_option$(v2) = v1) | ~ (matrix_to_iarray_option$(v2) = % 74.23/10.91 v0)) & ! [v0: A_iarray_iarray_option$] : ! [v1: A_iarray_iarray_option$] % 74.23/10.91 : ! [v2: A_iarray_iarray$] : (v1 = v0 | ~ (inverse_matrix_iarray$(v2) = v1) % 74.23/10.91 | ~ (inverse_matrix_iarray$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v1: % 74.23/10.91 A_iarray_iarray_a_iarray_iarray_prod$] : ! [v2: A_iarray_iarray$] : (v1 = % 74.23/10.91 v0 | ~ (gauss_Jordan_iarrays_PA$(v2) = v1) | ~ % 74.23/10.91 (gauss_Jordan_iarrays_PA$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 74.23/10.91 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan$(v2) % 74.23/10.91 = v1) | ~ (gauss_Jordan$(v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: % 74.23/10.91 A_iarray_iarray$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ % 74.23/10.91 (matrix_to_iarray$(v2) = v1) | ~ (matrix_to_iarray$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_list_a_iarray_list_fun$] : ! [v1: % 74.23/10.91 A_iarray_list_a_iarray_list_fun$] : ! [v2: A_iarray_bool_fun$] : (v1 = v0 | % 74.23/10.91 ~ (filter$(v2) = v1) | ~ (filter$(v2) = v0)) & ! [v0: A_iarray_iarray$] : % 74.23/10.91 ! [v1: A_iarray_iarray$] : ! [v2: A_iarray_iarray$] : (v1 = v0 | ~ % 74.23/10.91 (gauss_Jordan_iarrays$(v2) = v1) | ~ (gauss_Jordan_iarrays$(v2) = v0)) & ! % 74.23/10.91 [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: A_iarray_iarray$] : % 74.23/10.91 (v1 = v0 | ~ (list_of$(v2) = v1) | ~ (list_of$(v2) = v0)) & ! [v0: % 74.23/10.91 A_iarray_iarray_option$] : ! [v1: A_iarray_iarray_option$] : ! [v2: % 74.23/10.91 A_iarray_iarray$] : (v1 = v0 | ~ (some$(v2) = v1) | ~ (some$(v2) = v0)) & % 74.23/10.91 ! [v0: A_n_vec_n_vec_option$] : ! [v1: A_n_vec_n_vec_option$] : ! [v2: % 74.23/10.91 A_n_vec_n_vec$] : (v1 = v0 | ~ (some$a(v2) = v1) | ~ (some$a(v2) = v0)) & % 74.23/10.92 ! [v0: Int_int_bool_fun_fun$] : ! [v1: Int_int_bool_fun_fun$] : ! [v2: % 74.23/10.92 Int_int_prod_set$] : (v1 = v0 | ~ (uuo$(v2) = v1) | ~ (uuo$(v2) = v0)) & % 74.23/10.92 ! [v0: A_iarray_list_a_iarray_list_bool_fun_fun$] : ! [v1: % 74.23/10.92 A_iarray_list_a_iarray_list_bool_fun_fun$] : ! [v2: % 74.23/10.92 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (uuq$(v2) = v1) | ~ % 74.23/10.92 (uuq$(v2) = v0)) & ! [v0: A_iarray_a_iarray_bool_fun_fun$] : ! [v1: % 74.23/10.92 A_iarray_a_iarray_bool_fun_fun$] : ! [v2: A_iarray_a_iarray_prod_set$] : % 74.23/10.92 (v1 = v0 | ~ (uur$(v2) = v1) | ~ (uur$(v2) = v0)) & ! [v0: % 74.23/10.92 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v1: % 74.23/10.92 A_iarray_iarray_a_iarray_iarray_bool_fun_fun$] : ! [v2: % 74.23/10.92 A_iarray_iarray_a_iarray_iarray_prod_set$] : (v1 = v0 | ~ (uup$(v2) = v1) | % 74.23/10.92 ~ (uup$(v2) = v0)) & ! [v0: A_iarray_set$] : ! [v1: A_iarray_set$] : ! % 74.23/10.92 [v2: A_iarray_list$] : (v1 = v0 | ~ (set$(v2) = v1) | ~ (set$(v2) = v0)) & % 74.23/10.92 ! [v0: A_iarray_list_bool_fun$] : ! [v1: A_iarray_list_bool_fun$] : ! [v2: % 74.23/10.92 A_iarray_list_bool_fun$] : (v1 = v0 | ~ (uuc$(v2) = v1) | ~ (uuc$(v2) = % 74.23/10.92 v0)) & ! [v0: A_iarray_bool_fun$] : ! [v1: A_iarray_bool_fun$] : ! [v2: % 74.23/10.92 A_iarray_bool_fun$] : (v1 = v0 | ~ (uud$(v2) = v1) | ~ (uud$(v2) = v0)) & % 74.23/10.92 ! [v0: Nat_a_iarray_prod_bool_fun$] : ! [v1: Nat_a_iarray_prod_bool_fun$] : % 74.23/10.92 ! [v2: Nat_a_iarray_prod_bool_fun$] : (v1 = v0 | ~ (uub$(v2) = v1) | ~ % 74.23/10.92 (uub$(v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: Int_bool_fun$] : ! [v2: % 74.23/10.92 Int_set$] : (v1 = v0 | ~ (uul$(v2) = v1) | ~ (uul$(v2) = v0)) & ! [v0: % 74.23/10.92 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : (v1 = v0 | ~ % 74.23/10.92 (uum$(v2) = v1) | ~ (uum$(v2) = v0)) & ! [v0: A_iarray_list_bool_fun$] : % 74.23/10.92 ! [v1: A_iarray_list_bool_fun$] : ! [v2: A_iarray_list_set$] : (v1 = v0 | ~ % 74.23/10.92 (uuk$(v2) = v1) | ~ (uuk$(v2) = v0)) & ! [v0: A_iarray_bool_fun$] : ! % 74.23/10.92 [v1: A_iarray_bool_fun$] : ! [v2: A_iarray_set$] : (v1 = v0 | ~ (uun$(v2) = % 74.23/10.92 v1) | ~ (uun$(v2) = v0)) & ! [v0: % 74.23/10.92 A_iarray_list_a_iarray_list_prod_bool_fun$] : ! [v1: % 74.23/10.92 A_iarray_list_a_iarray_list_prod_bool_fun$] : ! [v2: % 74.23/10.92 A_iarray_list_a_iarray_list_prod_set$] : (v1 = v0 | ~ (uuj$(v2) = v1) | ~ % 74.23/10.92 (uuj$(v2) = v0)) % 74.23/10.92 % 74.23/10.92 Further assumptions not needed in the proof: % 74.23/10.92 -------------------------------------------- % 74.23/10.92 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 74.23/10.92 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 74.23/10.92 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 74.23/10.92 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 74.23/10.92 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 74.23/10.92 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 74.23/10.92 axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, % 74.23/10.92 axiom149, axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 74.23/10.92 axiom156, axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, % 74.23/10.92 axiom163, axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, % 74.23/10.92 axiom170, axiom172, axiom173, axiom174, axiom175, axiom177, axiom178, axiom179, % 74.23/10.92 axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, % 74.23/10.92 axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 74.23/10.92 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 74.23/10.92 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 74.23/10.92 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 74.23/10.92 axiom215, axiom216, axiom217, axiom218, axiom219, axiom220, axiom221, axiom222, % 74.23/10.92 axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, axiom23, % 74.23/10.92 axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, axiom237, % 74.23/10.92 axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, axiom244, % 74.23/10.92 axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, axiom251, % 74.23/10.92 axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, % 74.23/10.92 axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, axiom266, % 74.23/10.92 axiom267, axiom268, axiom269, axiom270, axiom271, axiom272, axiom273, axiom274, % 74.23/10.92 axiom275, axiom276, axiom277, axiom278, axiom279, axiom280, axiom281, axiom282, % 74.23/10.92 axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, axiom289, axiom29, % 74.23/10.92 axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, axiom297, % 74.23/10.92 axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, axiom303, % 74.23/10.92 axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, axiom310, % 74.23/10.92 axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, axiom317, axiom318, % 74.23/10.92 axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, axiom325, % 74.23/10.92 axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, axiom332, % 74.23/10.92 axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, % 74.23/10.92 axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, % 74.23/10.92 axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, % 74.23/10.92 axiom355, axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, % 74.23/10.92 axiom362, axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, % 74.23/10.92 axiom37, axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, % 74.23/10.92 axiom377, axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, % 74.23/10.92 axiom384, axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, % 74.23/10.92 axiom391, axiom392, axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, % 74.23/10.92 axiom399, axiom4, axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, % 74.23/10.92 axiom405, axiom406, axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, % 74.23/10.92 axiom412, axiom413, axiom414, axiom415, axiom416, axiom417, axiom42, axiom421, % 74.23/10.92 axiom423, axiom424, axiom425, axiom426, axiom427, axiom428, axiom429, axiom43, % 74.23/10.92 axiom430, axiom431, axiom432, axiom433, axiom434, axiom435, axiom436, axiom437, % 74.23/10.92 axiom438, axiom439, axiom44, axiom440, axiom441, axiom442, axiom443, axiom444, % 74.23/10.92 axiom445, axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, axiom454, % 74.23/10.92 axiom455, axiom456, axiom457, axiom458, axiom459, axiom46, axiom460, axiom461, % 74.23/10.92 axiom462, axiom463, axiom464, axiom465, axiom466, axiom467, axiom468, axiom469, % 74.23/10.92 axiom47, axiom470, axiom471, axiom472, axiom473, axiom474, axiom475, axiom476, % 74.23/10.92 axiom477, axiom478, axiom479, axiom48, axiom480, axiom481, axiom482, axiom483, % 74.23/10.92 axiom484, axiom485, axiom486, axiom487, axiom488, axiom489, axiom49, axiom490, % 74.23/10.92 axiom491, axiom492, axiom493, axiom494, axiom495, axiom496, axiom497, axiom498, % 74.23/10.92 axiom499, axiom5, axiom50, axiom500, axiom501, axiom502, axiom503, axiom504, % 74.23/10.92 axiom505, axiom506, axiom507, axiom508, axiom509, axiom51, axiom510, axiom511, % 74.23/10.92 axiom512, axiom513, axiom514, axiom515, axiom516, axiom517, axiom518, axiom519, % 74.23/10.92 axiom52, axiom520, axiom521, axiom522, axiom523, axiom524, axiom525, axiom526, % 74.23/10.92 axiom527, axiom528, axiom529, axiom53, axiom530, axiom531, axiom532, axiom533, % 74.23/10.92 axiom534, axiom535, axiom536, axiom537, axiom538, axiom539, axiom54, axiom540, % 74.23/10.92 axiom541, axiom542, axiom543, axiom544, axiom545, axiom546, axiom547, axiom548, % 74.23/10.92 axiom549, axiom55, axiom550, axiom551, axiom552, axiom553, axiom554, axiom555, % 74.23/10.92 axiom556, axiom557, axiom558, axiom559, axiom56, axiom560, axiom561, axiom562, % 74.23/10.92 axiom563, axiom564, axiom565, axiom566, axiom567, axiom568, axiom569, axiom57, % 74.23/10.92 axiom570, axiom571, axiom572, axiom573, axiom574, axiom575, axiom576, axiom577, % 74.23/10.92 axiom578, axiom579, axiom58, axiom580, axiom581, axiom582, axiom583, axiom584, % 74.23/10.92 axiom586, axiom587, axiom588, axiom589, axiom59, axiom590, axiom591, axiom592, % 74.23/10.92 axiom593, axiom594, axiom595, axiom596, axiom597, axiom598, axiom599, axiom6, % 74.23/10.92 axiom60, axiom600, axiom601, axiom602, axiom603, axiom604, axiom605, axiom606, % 74.23/10.92 axiom607, axiom608, axiom609, axiom61, axiom610, axiom611, axiom612, axiom613, % 74.23/10.92 axiom614, axiom615, axiom616, axiom617, axiom618, axiom619, axiom62, axiom620, % 74.23/10.92 axiom621, axiom622, axiom623, axiom624, axiom626, axiom627, axiom628, axiom629, % 74.23/10.92 axiom63, axiom630, axiom632, axiom634, axiom635, axiom637, axiom639, axiom64, % 74.23/10.92 axiom640, axiom641, axiom642, axiom643, axiom644, axiom645, axiom646, axiom647, % 74.23/10.92 axiom648, axiom649, axiom65, axiom650, axiom66, axiom67, axiom68, axiom69, % 74.23/10.92 axiom7, axiom70, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, % 74.23/10.92 axiom78, axiom79, axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, % 74.23/10.92 axiom86, axiom87, axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, % 74.23/10.92 axiom94, axiom95, axiom96, axiom97, axiom98, axiom99, formula_652, formula_653, % 74.23/10.92 formula_654, formula_655, formula_656, formula_657, formula_658, formula_659, % 74.23/10.92 formula_660 % 74.23/10.92 % 74.23/10.92 Those formulas are unsatisfiable: % 74.23/10.92 --------------------------------- % 74.23/10.92 % 74.23/10.92 Begin of proof % 74.23/10.92 | % 74.23/10.92 | ALPHA: (axiom27) implies: % 74.23/10.92 | (1) ? [v0: A_iarray_list_a_iarray_list_fun$] : (filter$(uu$) = v0 & % 74.23/10.92 | A_iarray_list_a_iarray_list_fun$(v0) & ! [v1: A_iarray_iarray$] : ! % 74.23/10.92 | [v2: Nat$] : ( ~ (fun_app$q(rank_iarray$, v1) = v2) | ~ % 74.23/10.92 | A_iarray_iarray$(v1) | ? [v3: int] : ? [v4: A_iarray_iarray$] : % 74.23/10.92 | ? [v5: A_iarray_list$] : ? [v6: A_iarray_list$] : ? [v7: Nat$] : % 74.23/10.92 | (gauss_Jordan_iarrays$(v1) = v4 & list_of$(v4) = v5 & fun_app$p(v0, % 74.23/10.92 | v5) = v6 & fun_app$m(size$, v6) = v7 & fun_app$l(of_nat$, v7) = % 74.23/10.92 | v3 & fun_app$l(of_nat$, v2) = v3 & A_iarray_list$(v6) & % 74.23/10.92 | A_iarray_list$(v5) & Nat$(v7) & A_iarray_iarray$(v4)))) % 74.23/10.92 | % 74.23/10.92 | ALPHA: (axiom171) implies: % 74.23/10.92 | (2) ! [v0: Nat$] : ! [v1: A_iarray_list$] : ! [v2: % 74.23/10.92 | A_iarray_list_nat_fun$] : ! [v3: Nat$] : ( ~ (gen_length$b(v0) = v2) % 74.23/10.92 | | ~ (fun_app$m(v2, v1) = v3) | ~ A_iarray_list$(v1) | ~ Nat$(v0) | % 74.23/10.92 | ? [v4: int] : ? [v5: int] : ? [v6: Nat$] : (fun_app$m(size$, v1) = % 74.23/10.92 | v6 & fun_app$l(of_nat$, v6) = $difference(v4, v5) & % 74.23/10.92 | fun_app$l(of_nat$, v3) = v4 & fun_app$l(of_nat$, v0) = v5 & % 74.23/10.92 | Nat$(v6))) % 74.23/10.92 | % 74.23/10.92 | ALPHA: (axiom176) implies: % 74.23/10.92 | (3) ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: Nat$] : ! % 74.23/10.92 | [v3: Nat$] : ( ~ (fun_app$m(size$, v1) = v3) | ~ (fun_app$m(size$, v0) % 74.23/10.92 | = v2) | ~ A_iarray_list$(v1) | ~ A_iarray_list$(v0) | ? [v4: % 74.23/10.92 | A_iarray_list$] : ? [v5: Nat$] : ? [v6: int] : ? [v7: int] : % 74.23/10.92 | (splice$b(v0, v1) = v4 & fun_app$m(size$, v4) = v5 & % 74.23/10.92 | fun_app$l(of_nat$, v5) = v6 & fun_app$l(of_nat$, v3) = % 74.23/10.92 | $difference(v6, v7) & fun_app$l(of_nat$, v2) = v7 & % 74.23/10.92 | A_iarray_list$(v4) & Nat$(v5))) % 74.23/10.92 | % 74.23/10.92 | ALPHA: (axiom418) implies: % 74.23/10.92 | (4) ? [v0: Nat$] : (gen_length$(v0) = size$a & fun_app$k(nat$, 0) = v0 & % 74.23/10.92 | Nat$(v0)) % 74.23/10.92 | % 74.23/10.92 | ALPHA: (axiom419) implies: % 74.23/10.93 | (5) ? [v0: Nat$] : (gen_length$a(v0) = size$b & fun_app$k(nat$, 0) = v0 & % 74.23/10.93 | Nat$(v0)) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom420) implies: % 74.23/10.93 | (6) ? [v0: Nat$] : (gen_length$b(v0) = size$ & fun_app$k(nat$, 0) = v0 & % 74.23/10.93 | Nat$(v0)) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom422) implies: % 74.23/10.93 | (7) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: % 74.23/10.93 | Nat_nat_bool_fun_fun$] : ! [v2: Nat$] : ! [v3: Nat$] : ! [v4: % 74.23/10.93 | Nat_bool_fun$] : ! [v5: int] : (v5 = 0 | ~ (fun_app$as(v1, v2) = % 74.23/10.93 | v4) | ~ (fun_app$c(v4, v3) = v5) | ~ Nat$(v3) | ~ Nat$(v2) | % 74.23/10.93 | ~ Nat_nat_bool_fun_fun$(v1) | ? [v6: Nat$] : ? [v7: Nat$] : ? % 74.23/10.93 | [v8: Nat_bool_fun$] : ? [v9: int] : ? [v10: int] : ? [v11: Nat$] % 74.23/10.93 | : ? [v12: int] : ( ~ (v12 = 0) & fun_app$as(v1, v6) = v8 & % 74.23/10.93 | fun_app$l(of_nat$, v7) = v10 & fun_app$l(of_nat$, v6) = v9 & % 74.23/10.93 | fun_app$k(nat$, $sum(v10, v9)) = v11 & fun_app$c(v8, v11) = v12 & % 74.23/10.93 | fun_app$c(v8, v7) = 0 & Nat_bool_fun$(v8) & Nat$(v11) & Nat$(v7) % 74.23/10.93 | & Nat$(v6)) | ? [v6: Nat$] : ? [v7: Nat$] : ? [v8: % 74.23/10.93 | Nat_bool_fun$] : ? [v9: any] : ? [v10: Nat_bool_fun$] : ? % 74.23/10.93 | [v11: any] : (fun_app$as(v1, v7) = v10 & fun_app$as(v1, v6) = v8 & % 74.23/10.93 | fun_app$c(v10, v6) = v11 & fun_app$c(v8, v7) = v9 & % 74.23/10.93 | Nat_bool_fun$(v10) & Nat_bool_fun$(v8) & Nat$(v7) & Nat$(v6) & ( % 74.23/10.93 | ~ (v11 = 0) | ~ (v9 = 0)) & (v11 = 0 | v9 = 0)) | ? [v6: % 74.23/10.93 | Nat$] : ? [v7: Nat_bool_fun$] : ? [v8: int] : ( ~ (v8 = 0) & % 74.23/10.93 | fun_app$as(v1, v6) = v7 & fun_app$c(v7, v0) = v8 & % 74.23/10.93 | Nat_bool_fun$(v7) & Nat$(v6)))) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom451) implies: % 74.23/10.93 | (8) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: % 74.23/10.93 | Nat_bool_fun$] : ! [v2: Nat$] : ( ~ (fun_app$c(v1, v2) = 0) | ~ % 74.23/10.93 | Nat_bool_fun$(v1) | ~ Nat$(v2) | fun_app$c(v1, v0) = 0 | ? [v3: % 74.23/10.93 | Nat$] : ? [v4: int] : ? [v5: Nat$] : ? [v6: int] : ( ~ (v6 = % 74.23/10.93 | 0) & fun_app$l(of_nat$, v3) = v4 & fun_app$k(nat$, $sum(v4, 1)) % 74.23/10.93 | = v5 & fun_app$c(v1, v5) = 0 & fun_app$c(v1, v3) = v6 & Nat$(v5) % 74.23/10.93 | & Nat$(v3)))) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom452) implies: % 74.23/10.93 | (9) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: % 74.23/10.93 | Nat_nat_bool_fun_fun$] : ! [v2: Nat$] : ! [v3: Nat$] : ! [v4: % 74.23/10.93 | Nat_bool_fun$] : ! [v5: int] : (v5 = 0 | ~ (fun_app$as(v1, v2) = % 74.23/10.93 | v4) | ~ (fun_app$c(v4, v3) = v5) | ~ Nat$(v3) | ~ Nat$(v2) | % 74.23/10.93 | ~ Nat_nat_bool_fun_fun$(v1) | ? [v6: Nat$] : ? [v7: Nat$] : ? % 74.23/10.93 | [v8: Nat_bool_fun$] : ? [v9: int] : ? [v10: Nat$] : ? [v11: % 74.23/10.93 | Nat_bool_fun$] : ? [v12: int] : ? [v13: Nat$] : ? [v14: int] : % 74.23/10.93 | ( ~ (v14 = 0) & fun_app$as(v1, v10) = v11 & fun_app$as(v1, v6) = v8 % 74.23/10.93 | & fun_app$l(of_nat$, v7) = v12 & fun_app$l(of_nat$, v6) = v9 & % 74.23/10.93 | fun_app$k(nat$, $sum(v12, 1)) = v13 & fun_app$k(nat$, $sum(v9, % 74.23/10.93 | 1)) = v10 & fun_app$c(v11, v13) = v14 & fun_app$c(v8, v7) = 0 % 74.23/10.93 | & Nat_bool_fun$(v11) & Nat_bool_fun$(v8) & Nat$(v13) & Nat$(v10) % 74.23/10.93 | & Nat$(v7) & Nat$(v6)) | ? [v6: Nat$] : ? [v7: Nat_bool_fun$] : % 74.23/10.93 | ? [v8: int] : ( ~ (v8 = 0) & fun_app$as(v1, v6) = v7 & % 74.23/10.93 | fun_app$c(v7, v0) = v8 & Nat_bool_fun$(v7) & Nat$(v6)) | ? [v6: % 74.23/10.93 | Nat_bool_fun$] : (fun_app$as(v1, v0) = v6 & Nat_bool_fun$(v6) & % 74.23/10.93 | ? [v7: Nat$] : ? [v8: int] : ? [v9: Nat$] : ? [v10: int] : ( ~ % 74.23/10.93 | (v10 = 0) & fun_app$l(of_nat$, v7) = v8 & fun_app$k(nat$, % 74.23/10.93 | $sum(v8, 1)) = v9 & fun_app$c(v6, v9) = v10 & Nat$(v9) & % 74.23/10.93 | Nat$(v7))))) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom453) implies: % 74.23/10.93 | (10) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: % 74.23/10.93 | Nat_bool_fun$] : ! [v2: Nat$] : ! [v3: int] : (v3 = 0 | ~ % 74.23/10.93 | (fun_app$c(v1, v2) = v3) | ~ Nat_bool_fun$(v1) | ~ Nat$(v2) | ? % 74.23/10.93 | [v4: Nat$] : ? [v5: int] : ? [v6: Nat$] : ? [v7: int] : ( ~ (v7 % 74.23/10.93 | = 0) & fun_app$l(of_nat$, v4) = v5 & fun_app$k(nat$, $sum(v5, % 74.23/10.93 | 1)) = v6 & fun_app$c(v1, v6) = v7 & fun_app$c(v1, v4) = 0 & % 74.23/10.93 | Nat$(v6) & Nat$(v4)) | ? [v4: int] : ( ~ (v4 = 0) & % 74.23/10.93 | fun_app$c(v1, v0) = v4))) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom585) implies: % 74.23/10.93 | (11) ? [v0: Nat$] : (fun_app$m(size$, nil$) = v0 & fun_app$l(of_nat$, v0) % 74.23/10.93 | = 0 & Nat$(v0)) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom625) implies: % 74.23/10.93 | (12) A_iarray_list$(nil$) % 74.23/10.93 | % 74.23/10.93 | ALPHA: (axiom631) implies: % 74.23/10.94 | (13) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: Nat$] : % 74.23/10.94 | ! [v2: Nat_bool_fun$] : ! [v3: int] : ! [v4: any] : ( ~ % 74.23/10.94 | (fun_app$l(of_nat$, v1) = v3) | ~ (fun_app$c(v2, v0) = v4) | ~ % 74.23/10.94 | Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: Nat$] : ? [v6: int] : % 74.23/10.94 | ? [v7: int] : ( ~ (v7 = 0) & $lesseq(v6, v3) & fun_app$l(of_nat$, % 74.23/10.94 | v5) = v6 & fun_app$c(v2, v5) = v7 & Nat$(v5)) | (v4 = 0 & ! % 74.23/10.94 | [v5: Nat$] : ! [v6: int] : ! [v7: Nat$] : ! [v8: int] : (v8 = % 74.23/10.94 | 0 | ~ ($lesseq(1, $difference(v3, v6))) | ~ % 74.23/10.94 | (fun_app$l(of_nat$, v5) = v6) | ~ (fun_app$k(nat$, $sum(v6, % 74.23/10.94 | 1)) = v7) | ~ (fun_app$c(v2, v7) = v8) | ~ Nat$(v5)))) % 74.23/10.94 | & ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : ! [v3: int] : ( ~ % 74.23/10.94 | (fun_app$l(of_nat$, v1) = v3) | ~ (fun_app$c(v2, v0) = 0) | ~ % 74.23/10.94 | Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v4: Nat$] : ? [v5: int] : % 74.23/10.94 | ? [v6: Nat$] : ? [v7: int] : ( ~ (v7 = 0) & $lesseq(1, % 74.23/10.94 | $difference(v3, v5)) & fun_app$l(of_nat$, v4) = v5 & % 74.23/10.94 | fun_app$k(nat$, $sum(v5, 1)) = v6 & fun_app$c(v2, v6) = v7 & % 74.23/10.94 | Nat$(v6) & Nat$(v4)) | ! [v4: Nat$] : ! [v5: int] : ( ~ % 74.23/10.94 | ($lesseq(v5, v3)) | ~ (fun_app$l(of_nat$, v4) = v5) | ~ % 74.23/10.94 | Nat$(v4) | fun_app$c(v2, v4) = 0))) % 74.23/10.94 | % 74.23/10.94 | ALPHA: (axiom633) implies: % 74.23/10.94 | (14) ? [v0: Nat$] : (fun_app$k(nat$, 0) = v0 & Nat$(v0) & ! [v1: Nat$] : % 74.23/10.94 | ! [v2: Nat_bool_fun$] : ! [v3: int] : ! [v4: int] : (v4 = 0 | ~ % 74.23/10.94 | (fun_app$l(of_nat$, v1) = v3) | ~ (fun_app$c(v2, v0) = v4) | ~ % 74.23/10.94 | Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: Nat$] : ? [v6: int] : % 74.23/10.94 | ? [v7: Nat$] : ($lesseq(1, $difference(v3, v6)) & % 74.23/10.94 | fun_app$l(of_nat$, v5) = v6 & fun_app$k(nat$, $sum(v6, 1)) = v7 % 74.23/10.94 | & fun_app$c(v2, v7) = 0 & Nat$(v7) & Nat$(v5)) | ! [v5: Nat$] : % 74.23/10.94 | ! [v6: int] : ( ~ ($lesseq(v6, v3)) | ~ (fun_app$l(of_nat$, v5) % 74.23/10.94 | = v6) | ~ Nat$(v5) | ? [v7: int] : ( ~ (v7 = 0) & % 74.23/10.94 | fun_app$c(v2, v5) = v7))) & ! [v1: Nat$] : ! [v2: % 74.23/10.94 | Nat_bool_fun$] : ! [v3: any] : ! [v4: int] : ( ~ % 74.23/10.94 | (fun_app$l(of_nat$, v1) = v4) | ~ (fun_app$c(v2, v0) = v3) | ~ % 74.23/10.94 | Nat_bool_fun$(v2) | ~ Nat$(v1) | ? [v5: Nat$] : ? [v6: int] : % 74.23/10.94 | ($lesseq(v6, v4) & fun_app$l(of_nat$, v5) = v6 & fun_app$c(v2, v5) % 74.23/10.94 | = 0 & Nat$(v5)) | ( ~ (v3 = 0) & ! [v5: Nat$] : ! [v6: int] : % 74.23/10.94 | ! [v7: Nat$] : ( ~ ($lesseq(1, $difference(v4, v6))) | ~ % 74.23/10.94 | (fun_app$l(of_nat$, v5) = v6) | ~ (fun_app$k(nat$, $sum(v6, % 74.23/10.94 | 1)) = v7) | ~ (fun_app$c(v2, v7) = 0) | ~ Nat$(v5))))) % 74.23/10.94 | % 74.23/10.94 | ALPHA: (axiom636) implies: % 74.23/10.94 | (15) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: int] : ( ~ % 74.23/10.94 | ($lesseq(v2, v3)) | ~ (fun_app$l(of_nat$, v1) = v2) | ~ % 74.23/10.94 | (fun_app$l(of_nat$, v0) = v3) | ~ Nat$(v1) | ~ Nat$(v0) | ! [v4: % 74.23/10.94 | Nat$] : ( ~ (fun_app$l(of_nat$, v4) = $sum($difference(v2, v3), % 74.23/10.94 | -1)) | ~ Nat$(v4))) % 74.23/10.94 | % 74.23/10.94 | ALPHA: (axiom638) implies: % 74.23/10.94 | (16) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: int] : ( ~ % 74.23/10.94 | ($lesseq(v3, -1)) | ~ (fun_app$l(of_nat$, v1) = v3) | ~ % 74.23/10.94 | (fun_app$l(of_nat$, v0) = v2) | ~ Nat$(v1) | ~ Nat$(v0)) % 74.23/10.94 | % 74.23/10.94 | ALPHA: (conjecture22) implies: % 74.23/10.94 | (17) A_n_vec_n_vec$(a$) % 74.23/10.95 | (18) ? [v0: A_iarray_list_a_iarray_list_fun$] : ? [v1: A_iarray_iarray$] % 74.23/10.95 | : ? [v2: A_iarray_iarray$] : ? [v3: A_iarray_list$] : ? [v4: % 74.23/10.95 | A_iarray_list$] : ? [v5: Nat$] : ? [v6: int] : ? [v7: Nat$] : ? % 74.23/10.95 | [v8: int] : ? [v9: A_n_vec_n_vec$] : ? [v10: A_iarray_iarray$] : ? % 74.23/10.95 | [v11: A_iarray_list$] : ? [v12: A_iarray_list$] : ? [v13: Nat$] : ? % 74.23/10.95 | [v14: int] : ? [v15: A_iarray_iarray_a_iarray_iarray_prod$] : ? % 74.23/10.95 | [v16: A_iarray_iarray$] : ? [v17: A_iarray_iarray_option$] : % 74.23/10.95 | (gauss_Jordan_iarrays_PA$(v1) = v15 & fun_app$r(fst$, v15) = v16 & % 74.23/10.95 | gauss_Jordan$(a$) = v9 & matrix_to_iarray$(v9) = v10 & % 74.23/10.95 | matrix_to_iarray$(a$) = v1 & filter$(uu$) = v0 & % 74.23/10.95 | fun_app$q(nrows_iarray$, v1) = v7 & gauss_Jordan_iarrays$(v1) = v2 & % 74.23/10.95 | list_of$(v10) = v11 & list_of$(v2) = v3 & fun_app$p(v0, v11) = v12 & % 74.23/10.95 | fun_app$p(v0, v3) = v4 & some$(v16) = v17 & fun_app$m(size$, v12) = % 74.23/10.95 | v13 & fun_app$m(size$, v4) = v5 & fun_app$l(of_nat$, v13) = v14 & % 74.23/10.95 | fun_app$l(of_nat$, v7) = v8 & fun_app$l(of_nat$, v5) = v6 & % 74.23/10.95 | A_iarray_list_a_iarray_list_fun$(v0) & A_iarray_list$(v12) & % 74.23/10.95 | A_iarray_list$(v11) & A_iarray_list$(v4) & A_iarray_list$(v3) & % 74.23/10.95 | A_iarray_iarray_option$(v17) & Nat$(v13) & Nat$(v7) & Nat$(v5) & % 74.23/10.95 | A_n_vec_n_vec$(v9) & A_iarray_iarray$(v16) & A_iarray_iarray$(v10) & % 74.23/10.95 | A_iarray_iarray$(v2) & A_iarray_iarray$(v1) & % 74.23/10.95 | A_iarray_iarray_a_iarray_iarray_prod$(v15) & ((v14 = v8 & ~ (v17 = % 74.23/10.95 | none$) & ~ (v8 = v6)) | (v8 = v6 & ~ (v17 = none$) & ~ (v14 % 74.23/10.95 | = v6)))) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (function-axioms) implies: % 74.23/10.95 | (19) ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: % 74.23/10.95 | A_iarray_iarray$] : (v1 = v0 | ~ (list_of$(v2) = v1) | ~ % 74.23/10.95 | (list_of$(v2) = v0)) % 74.23/10.95 | (20) ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 74.23/10.95 | A_iarray_iarray$] : (v1 = v0 | ~ (gauss_Jordan_iarrays$(v2) = v1) | % 74.23/10.95 | ~ (gauss_Jordan_iarrays$(v2) = v0)) % 74.23/10.95 | (21) ! [v0: A_iarray_list_a_iarray_list_fun$] : ! [v1: % 74.23/10.95 | A_iarray_list_a_iarray_list_fun$] : ! [v2: A_iarray_bool_fun$] : % 74.23/10.95 | (v1 = v0 | ~ (filter$(v2) = v1) | ~ (filter$(v2) = v0)) % 74.23/10.95 | (22) ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 74.23/10.95 | A_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_to_iarray$(v2) = v1) | ~ % 74.23/10.95 | (matrix_to_iarray$(v2) = v0)) % 74.23/10.95 | (23) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: Int_nat_fun$] : % 74.23/10.95 | (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) % 74.23/10.95 | (24) ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : ! [v3: Nat_int_fun$] : % 74.23/10.95 | (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) % 74.23/10.95 | (25) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_iarray_list$] : ! [v3: % 74.23/10.95 | A_iarray_list_nat_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) | % 74.23/10.95 | ~ (fun_app$m(v3, v2) = v0)) % 74.23/10.95 | (26) ! [v0: A_iarray_list$] : ! [v1: A_iarray_list$] : ! [v2: % 74.23/10.95 | A_iarray_list$] : ! [v3: A_iarray_list_a_iarray_list_fun$] : (v1 = % 74.23/10.95 | v0 | ~ (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (4) with fresh symbol all_793_0 gives: % 74.23/10.95 | (27) gen_length$(all_793_0) = size$a & fun_app$k(nat$, 0) = all_793_0 & % 74.23/10.95 | Nat$(all_793_0) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (27) implies: % 74.23/10.95 | (28) fun_app$k(nat$, 0) = all_793_0 % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (11) with fresh symbol all_795_0 gives: % 74.23/10.95 | (29) fun_app$m(size$, nil$) = all_795_0 & fun_app$l(of_nat$, all_795_0) = 0 % 74.23/10.95 | & Nat$(all_795_0) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (29) implies: % 74.23/10.95 | (30) Nat$(all_795_0) % 74.23/10.95 | (31) fun_app$l(of_nat$, all_795_0) = 0 % 74.23/10.95 | (32) fun_app$m(size$, nil$) = all_795_0 % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (5) with fresh symbol all_798_0 gives: % 74.23/10.95 | (33) gen_length$a(all_798_0) = size$b & fun_app$k(nat$, 0) = all_798_0 & % 74.23/10.95 | Nat$(all_798_0) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (33) implies: % 74.23/10.95 | (34) Nat$(all_798_0) % 74.23/10.95 | (35) fun_app$k(nat$, 0) = all_798_0 % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (6) with fresh symbol all_804_0 gives: % 74.23/10.95 | (36) gen_length$b(all_804_0) = size$ & fun_app$k(nat$, 0) = all_804_0 & % 74.23/10.95 | Nat$(all_804_0) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (36) implies: % 74.23/10.95 | (37) fun_app$k(nat$, 0) = all_804_0 % 74.23/10.95 | (38) gen_length$b(all_804_0) = size$ % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (8) with fresh symbol all_892_0 gives: % 74.23/10.95 | (39) fun_app$k(nat$, 0) = all_892_0 & Nat$(all_892_0) & ! [v0: % 74.23/10.95 | Nat_bool_fun$] : ! [v1: Nat$] : ( ~ (fun_app$c(v0, v1) = 0) | ~ % 74.23/10.95 | Nat_bool_fun$(v0) | ~ Nat$(v1) | fun_app$c(v0, all_892_0) = 0 | ? % 74.23/10.95 | [v2: Nat$] : ? [v3: int] : ? [v4: Nat$] : ? [v5: int] : ( ~ (v5 = % 74.23/10.95 | 0) & fun_app$l(of_nat$, v2) = v3 & fun_app$k(nat$, $sum(v3, 1)) % 74.23/10.95 | = v4 & fun_app$c(v0, v4) = 0 & fun_app$c(v0, v2) = v5 & Nat$(v4) & % 74.23/10.95 | Nat$(v2))) % 74.23/10.95 | % 74.23/10.95 | ALPHA: (39) implies: % 74.23/10.95 | (40) fun_app$k(nat$, 0) = all_892_0 % 74.23/10.95 | % 74.23/10.95 | DELTA: instantiating (1) with fresh symbol all_895_0 gives: % 74.23/10.96 | (41) filter$(uu$) = all_895_0 & A_iarray_list_a_iarray_list_fun$(all_895_0) % 74.23/10.96 | & ! [v0: A_iarray_iarray$] : ! [v1: Nat$] : ( ~ % 74.23/10.96 | (fun_app$q(rank_iarray$, v0) = v1) | ~ A_iarray_iarray$(v0) | ? % 74.23/10.96 | [v2: int] : ? [v3: A_iarray_iarray$] : ? [v4: A_iarray_list$] : ? % 74.23/10.96 | [v5: A_iarray_list$] : ? [v6: Nat$] : (gauss_Jordan_iarrays$(v0) = % 74.23/10.96 | v3 & list_of$(v3) = v4 & fun_app$p(all_895_0, v4) = v5 & % 74.23/10.96 | fun_app$m(size$, v5) = v6 & fun_app$l(of_nat$, v6) = v2 & % 74.23/10.96 | fun_app$l(of_nat$, v1) = v2 & A_iarray_list$(v5) & % 74.23/10.96 | A_iarray_list$(v4) & Nat$(v6) & A_iarray_iarray$(v3))) % 74.23/10.96 | % 74.23/10.96 | ALPHA: (41) implies: % 74.23/10.96 | (42) filter$(uu$) = all_895_0 % 74.23/10.96 | % 74.23/10.96 | DELTA: instantiating (10) with fresh symbol all_898_0 gives: % 74.23/10.96 | (43) fun_app$k(nat$, 0) = all_898_0 & Nat$(all_898_0) & ! [v0: % 74.23/10.96 | Nat_bool_fun$] : ! [v1: Nat$] : ! [v2: int] : (v2 = 0 | ~ % 74.23/10.96 | (fun_app$c(v0, v1) = v2) | ~ Nat_bool_fun$(v0) | ~ Nat$(v1) | ? % 74.23/10.96 | [v3: Nat$] : ? [v4: int] : ? [v5: Nat$] : ? [v6: int] : ( ~ (v6 = % 74.23/10.96 | 0) & fun_app$l(of_nat$, v3) = v4 & fun_app$k(nat$, $sum(v4, 1)) % 74.23/10.96 | = v5 & fun_app$c(v0, v5) = v6 & fun_app$c(v0, v3) = 0 & Nat$(v5) & % 74.23/10.96 | Nat$(v3)) | ? [v3: int] : ( ~ (v3 = 0) & fun_app$c(v0, all_898_0) % 74.23/10.96 | = v3)) % 74.23/10.96 | % 74.23/10.96 | ALPHA: (43) implies: % 74.23/10.96 | (44) fun_app$k(nat$, 0) = all_898_0 % 74.23/10.96 | % 74.23/10.96 | DELTA: instantiating (14) with fresh symbol all_901_0 gives: % 74.23/10.96 | (45) fun_app$k(nat$, 0) = all_901_0 & Nat$(all_901_0) & ! [v0: Nat$] : ! % 74.23/10.96 | [v1: Nat_bool_fun$] : ! [v2: int] : ! [v3: int] : (v3 = 0 | ~ % 74.23/10.96 | (fun_app$l(of_nat$, v0) = v2) | ~ (fun_app$c(v1, all_901_0) = v3) | % 74.23/10.96 | ~ Nat_bool_fun$(v1) | ~ Nat$(v0) | ? [v4: Nat$] : ? [v5: int] : % 74.23/10.96 | ? [v6: Nat$] : ($lesseq(1, $difference(v2, v5)) & fun_app$l(of_nat$, % 74.23/10.96 | v4) = v5 & fun_app$k(nat$, $sum(v5, 1)) = v6 & fun_app$c(v1, v6) % 74.23/10.96 | = 0 & Nat$(v6) & Nat$(v4)) | ! [v4: Nat$] : ! [v5: int] : ( ~ % 74.23/10.96 | ($lesseq(v5, v2)) | ~ (fun_app$l(of_nat$, v4) = v5) | ~ Nat$(v4) % 74.23/10.96 | | ? [v6: int] : ( ~ (v6 = 0) & fun_app$c(v1, v4) = v6))) & ! % 74.23/10.96 | [v0: Nat$] : ! [v1: Nat_bool_fun$] : ! [v2: any] : ! [v3: int] : ( % 74.23/10.96 | ~ (fun_app$l(of_nat$, v0) = v3) | ~ (fun_app$c(v1, all_901_0) = v2) % 74.23/10.96 | | ~ Nat_bool_fun$(v1) | ~ Nat$(v0) | ? [v4: Nat$] : ? [v5: int] % 74.23/10.96 | : ($lesseq(v5, v3) & fun_app$l(of_nat$, v4) = v5 & fun_app$c(v1, v4) % 74.23/10.96 | = 0 & Nat$(v4)) | ( ~ (v2 = 0) & ! [v4: Nat$] : ! [v5: int] : ! % 74.23/10.96 | [v6: Nat$] : ( ~ ($lesseq(1, $difference(v3, v5))) | ~ % 74.23/10.96 | (fun_app$l(of_nat$, v4) = v5) | ~ (fun_app$k(nat$, $sum(v5, 1)) % 74.23/10.96 | = v6) | ~ (fun_app$c(v1, v6) = 0) | ~ Nat$(v4)))) % 74.23/10.96 | % 74.23/10.96 | ALPHA: (45) implies: % 74.23/10.96 | (46) fun_app$k(nat$, 0) = all_901_0 % 74.23/10.96 | % 74.23/10.96 | DELTA: instantiating (13) with fresh symbol all_904_0 gives: % 74.23/10.96 | (47) fun_app$k(nat$, 0) = all_904_0 & Nat$(all_904_0) & ! [v0: Nat$] : ! % 74.23/10.96 | [v1: Nat_bool_fun$] : ! [v2: int] : ! [v3: any] : ( ~ % 74.23/10.96 | (fun_app$l(of_nat$, v0) = v2) | ~ (fun_app$c(v1, all_904_0) = v3) | % 74.23/10.96 | ~ Nat_bool_fun$(v1) | ~ Nat$(v0) | ? [v4: Nat$] : ? [v5: int] : % 74.23/10.96 | ? [v6: int] : ( ~ (v6 = 0) & $lesseq(v5, v2) & fun_app$l(of_nat$, % 74.23/10.96 | v4) = v5 & fun_app$c(v1, v4) = v6 & Nat$(v4)) | (v3 = 0 & ! % 74.23/10.96 | [v4: Nat$] : ! [v5: int] : ! [v6: Nat$] : ! [v7: int] : (v7 = 0 % 74.23/10.96 | | ~ ($lesseq(1, $difference(v2, v5))) | ~ (fun_app$l(of_nat$, % 74.23/10.96 | v4) = v5) | ~ (fun_app$k(nat$, $sum(v5, 1)) = v6) | ~ % 74.23/10.96 | (fun_app$c(v1, v6) = v7) | ~ Nat$(v4)))) & ! [v0: Nat$] : ! % 74.23/10.96 | [v1: Nat_bool_fun$] : ! [v2: int] : ( ~ (fun_app$l(of_nat$, v0) = v2) % 74.23/10.96 | | ~ (fun_app$c(v1, all_904_0) = 0) | ~ Nat_bool_fun$(v1) | ~ % 74.23/10.96 | Nat$(v0) | ? [v3: Nat$] : ? [v4: int] : ? [v5: Nat$] : ? [v6: % 74.23/10.96 | int] : ( ~ (v6 = 0) & $lesseq(1, $difference(v2, v4)) & % 74.23/10.96 | fun_app$l(of_nat$, v3) = v4 & fun_app$k(nat$, $sum(v4, 1)) = v5 & % 74.23/10.96 | fun_app$c(v1, v5) = v6 & Nat$(v5) & Nat$(v3)) | ! [v3: Nat$] : ! % 74.23/10.96 | [v4: int] : ( ~ ($lesseq(v4, v2)) | ~ (fun_app$l(of_nat$, v3) = v4) % 74.23/10.96 | | ~ Nat$(v3) | fun_app$c(v1, v3) = 0)) % 74.23/10.96 | % 74.23/10.96 | ALPHA: (47) implies: % 74.23/10.96 | (48) fun_app$k(nat$, 0) = all_904_0 % 74.23/10.96 | % 74.23/10.96 | DELTA: instantiating (9) with fresh symbol all_907_0 gives: % 74.61/10.97 | (49) fun_app$k(nat$, 0) = all_907_0 & Nat$(all_907_0) & ! [v0: % 74.61/10.97 | Nat_nat_bool_fun_fun$] : ! [v1: Nat$] : ! [v2: Nat$] : ! [v3: % 74.61/10.97 | Nat_bool_fun$] : ! [v4: int] : (v4 = 0 | ~ (fun_app$as(v0, v1) = % 74.61/10.97 | v3) | ~ (fun_app$c(v3, v2) = v4) | ~ Nat$(v2) | ~ Nat$(v1) | ~ % 74.61/10.97 | Nat_nat_bool_fun_fun$(v0) | ? [v5: Nat$] : ? [v6: Nat$] : ? [v7: % 74.61/10.97 | Nat_bool_fun$] : ? [v8: int] : ? [v9: Nat$] : ? [v10: % 74.61/10.97 | Nat_bool_fun$] : ? [v11: int] : ? [v12: Nat$] : ? [v13: int] : % 74.61/10.97 | ( ~ (v13 = 0) & fun_app$as(v0, v9) = v10 & fun_app$as(v0, v5) = v7 & % 74.61/10.97 | fun_app$l(of_nat$, v6) = v11 & fun_app$l(of_nat$, v5) = v8 & % 74.61/10.97 | fun_app$k(nat$, $sum(v11, 1)) = v12 & fun_app$k(nat$, $sum(v8, 1)) % 74.61/10.97 | = v9 & fun_app$c(v10, v12) = v13 & fun_app$c(v7, v6) = 0 & % 74.61/10.97 | Nat_bool_fun$(v10) & Nat_bool_fun$(v7) & Nat$(v12) & Nat$(v9) & % 74.61/10.97 | Nat$(v6) & Nat$(v5)) | ? [v5: Nat$] : ? [v6: Nat_bool_fun$] : ? % 74.61/10.97 | [v7: int] : ( ~ (v7 = 0) & fun_app$as(v0, v5) = v6 & fun_app$c(v6, % 74.61/10.97 | all_907_0) = v7 & Nat_bool_fun$(v6) & Nat$(v5)) | ? [v5: % 74.61/10.97 | Nat_bool_fun$] : (fun_app$as(v0, all_907_0) = v5 & % 74.61/10.97 | Nat_bool_fun$(v5) & ? [v6: Nat$] : ? [v7: int] : ? [v8: Nat$] : % 74.61/10.97 | ? [v9: int] : ( ~ (v9 = 0) & fun_app$l(of_nat$, v6) = v7 & % 74.61/10.97 | fun_app$k(nat$, $sum(v7, 1)) = v8 & fun_app$c(v5, v8) = v9 & % 74.61/10.97 | Nat$(v8) & Nat$(v6)))) % 74.61/10.97 | % 74.61/10.97 | ALPHA: (49) implies: % 74.61/10.97 | (50) fun_app$k(nat$, 0) = all_907_0 % 74.61/10.97 | % 74.61/10.97 | DELTA: instantiating (7) with fresh symbol all_910_0 gives: % 74.61/10.97 | (51) fun_app$k(nat$, 0) = all_910_0 & Nat$(all_910_0) & ! [v0: % 74.61/10.97 | Nat_nat_bool_fun_fun$] : ! [v1: Nat$] : ! [v2: Nat$] : ! [v3: % 74.61/10.97 | Nat_bool_fun$] : ! [v4: int] : (v4 = 0 | ~ (fun_app$as(v0, v1) = % 74.61/10.97 | v3) | ~ (fun_app$c(v3, v2) = v4) | ~ Nat$(v2) | ~ Nat$(v1) | ~ % 74.61/10.97 | Nat_nat_bool_fun_fun$(v0) | ? [v5: Nat$] : ? [v6: Nat$] : ? [v7: % 74.61/10.97 | Nat_bool_fun$] : ? [v8: int] : ? [v9: int] : ? [v10: Nat$] : ? % 74.61/10.97 | [v11: int] : ( ~ (v11 = 0) & fun_app$as(v0, v5) = v7 & % 74.61/10.97 | fun_app$l(of_nat$, v6) = v9 & fun_app$l(of_nat$, v5) = v8 & % 74.61/10.97 | fun_app$k(nat$, $sum(v9, v8)) = v10 & fun_app$c(v7, v10) = v11 & % 74.61/10.97 | fun_app$c(v7, v6) = 0 & Nat_bool_fun$(v7) & Nat$(v10) & Nat$(v6) & % 74.61/10.97 | Nat$(v5)) | ? [v5: Nat$] : ? [v6: Nat$] : ? [v7: Nat_bool_fun$] % 74.61/10.97 | : ? [v8: any] : ? [v9: Nat_bool_fun$] : ? [v10: any] : % 74.61/10.97 | (fun_app$as(v0, v6) = v9 & fun_app$as(v0, v5) = v7 & fun_app$c(v9, % 74.61/10.97 | v5) = v10 & fun_app$c(v7, v6) = v8 & Nat_bool_fun$(v9) & % 74.61/10.97 | Nat_bool_fun$(v7) & Nat$(v6) & Nat$(v5) & ( ~ (v10 = 0) | ~ (v8 = % 74.61/10.97 | 0)) & (v10 = 0 | v8 = 0)) | ? [v5: Nat$] : ? [v6: % 74.61/10.97 | Nat_bool_fun$] : ? [v7: int] : ( ~ (v7 = 0) & fun_app$as(v0, v5) % 74.61/10.97 | = v6 & fun_app$c(v6, all_910_0) = v7 & Nat_bool_fun$(v6) & % 74.61/10.97 | Nat$(v5))) % 74.61/10.97 | % 74.61/10.97 | ALPHA: (51) implies: % 74.61/10.97 | (52) fun_app$k(nat$, 0) = all_910_0 % 74.61/10.97 | % 74.61/10.97 | DELTA: instantiating (18) with fresh symbols all_913_0, all_913_1, all_913_2, % 74.61/10.97 | all_913_3, all_913_4, all_913_5, all_913_6, all_913_7, all_913_8, % 74.61/10.97 | all_913_9, all_913_10, all_913_11, all_913_12, all_913_13, all_913_14, % 74.61/10.97 | all_913_15, all_913_16, all_913_17 gives: % 74.61/10.97 | (53) gauss_Jordan_iarrays_PA$(all_913_16) = all_913_2 & fun_app$r(fst$, % 74.61/10.97 | all_913_2) = all_913_1 & gauss_Jordan$(a$) = all_913_8 & % 74.61/10.97 | matrix_to_iarray$(all_913_8) = all_913_7 & matrix_to_iarray$(a$) = % 74.61/10.97 | all_913_16 & filter$(uu$) = all_913_17 & fun_app$q(nrows_iarray$, % 74.61/10.97 | all_913_16) = all_913_10 & gauss_Jordan_iarrays$(all_913_16) = % 74.61/10.97 | all_913_15 & list_of$(all_913_7) = all_913_6 & list_of$(all_913_15) = % 74.61/10.97 | all_913_14 & fun_app$p(all_913_17, all_913_6) = all_913_5 & % 74.61/10.97 | fun_app$p(all_913_17, all_913_14) = all_913_13 & some$(all_913_1) = % 74.61/10.97 | all_913_0 & fun_app$m(size$, all_913_5) = all_913_4 & fun_app$m(size$, % 74.61/10.97 | all_913_13) = all_913_12 & fun_app$l(of_nat$, all_913_4) = all_913_3 % 74.61/10.97 | & fun_app$l(of_nat$, all_913_10) = all_913_9 & fun_app$l(of_nat$, % 74.61/10.97 | all_913_12) = all_913_11 & % 74.61/10.97 | A_iarray_list_a_iarray_list_fun$(all_913_17) & % 74.61/10.97 | A_iarray_list$(all_913_5) & A_iarray_list$(all_913_6) & % 74.61/10.97 | A_iarray_list$(all_913_13) & A_iarray_list$(all_913_14) & % 74.61/10.97 | A_iarray_iarray_option$(all_913_0) & Nat$(all_913_4) & % 74.61/10.97 | Nat$(all_913_10) & Nat$(all_913_12) & A_n_vec_n_vec$(all_913_8) & % 74.61/10.97 | A_iarray_iarray$(all_913_1) & A_iarray_iarray$(all_913_7) & % 74.61/10.97 | A_iarray_iarray$(all_913_15) & A_iarray_iarray$(all_913_16) & % 74.61/10.97 | A_iarray_iarray_a_iarray_iarray_prod$(all_913_2) & ((all_913_3 = % 74.61/10.97 | all_913_9 & ~ (all_913_0 = none$) & ~ (all_913_9 = all_913_11)) % 74.61/10.97 | | (all_913_9 = all_913_11 & ~ (all_913_0 = none$) & ~ (all_913_3 = % 74.61/10.97 | all_913_11))) % 74.61/10.97 | % 74.61/10.97 | ALPHA: (53) implies: % 74.61/10.97 | (54) Nat$(all_913_10) % 74.61/10.97 | (55) Nat$(all_913_4) % 74.61/10.97 | (56) A_iarray_list$(all_913_13) % 74.61/10.97 | (57) A_iarray_list$(all_913_5) % 74.61/10.97 | (58) fun_app$l(of_nat$, all_913_12) = all_913_11 % 74.61/10.97 | (59) fun_app$l(of_nat$, all_913_10) = all_913_9 % 74.61/10.97 | (60) fun_app$l(of_nat$, all_913_4) = all_913_3 % 74.61/10.97 | (61) fun_app$m(size$, all_913_13) = all_913_12 % 74.61/10.97 | (62) fun_app$m(size$, all_913_5) = all_913_4 % 74.61/10.97 | (63) fun_app$p(all_913_17, all_913_14) = all_913_13 % 74.61/10.97 | (64) fun_app$p(all_913_17, all_913_6) = all_913_5 % 74.61/10.97 | (65) list_of$(all_913_15) = all_913_14 % 74.61/10.97 | (66) list_of$(all_913_7) = all_913_6 % 74.61/10.97 | (67) gauss_Jordan_iarrays$(all_913_16) = all_913_15 % 74.61/10.97 | (68) filter$(uu$) = all_913_17 % 74.61/10.97 | (69) matrix_to_iarray$(a$) = all_913_16 % 74.61/10.97 | (70) matrix_to_iarray$(all_913_8) = all_913_7 % 74.61/10.97 | (71) gauss_Jordan$(a$) = all_913_8 % 74.61/10.97 | (72) (all_913_3 = all_913_9 & ~ (all_913_0 = none$) & ~ (all_913_9 = % 74.61/10.97 | all_913_11)) | (all_913_9 = all_913_11 & ~ (all_913_0 = none$) & % 74.61/10.97 | ~ (all_913_3 = all_913_11)) % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_798_0, all_804_0, 0, nat$, % 74.61/10.97 | simplifying with (35), (37) gives: % 74.61/10.97 | (73) all_804_0 = all_798_0 % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_804_0, all_892_0, 0, nat$, % 74.61/10.97 | simplifying with (37), (40) gives: % 74.61/10.97 | (74) all_892_0 = all_804_0 % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_901_0, all_904_0, 0, nat$, % 74.61/10.97 | simplifying with (46), (48) gives: % 74.61/10.97 | (75) all_904_0 = all_901_0 % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_892_0, all_904_0, 0, nat$, % 74.61/10.97 | simplifying with (40), (48) gives: % 74.61/10.97 | (76) all_904_0 = all_892_0 % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_901_0, all_907_0, 0, nat$, % 74.61/10.97 | simplifying with (46), (50) gives: % 74.61/10.97 | (77) all_907_0 = all_901_0 % 74.61/10.97 | % 74.61/10.97 | GROUND_INST: instantiating (23) with all_793_0, all_907_0, 0, nat$, % 74.61/10.97 | simplifying with (28), (50) gives: % 74.61/10.97 | (78) all_907_0 = all_793_0 % 74.61/10.97 | % 74.61/10.98 | GROUND_INST: instantiating (23) with all_904_0, all_910_0, 0, nat$, % 74.61/10.98 | simplifying with (48), (52) gives: % 74.61/10.98 | (79) all_910_0 = all_904_0 % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (23) with all_898_0, all_910_0, 0, nat$, % 74.61/10.98 | simplifying with (44), (52) gives: % 74.61/10.98 | (80) all_910_0 = all_898_0 % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (21) with all_895_0, all_913_17, uu$, simplifying % 74.61/10.98 | with (42), (68) gives: % 74.61/10.98 | (81) all_913_17 = all_895_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (79), (80) imply: % 74.61/10.98 | (82) all_904_0 = all_898_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (82) implies: % 74.61/10.98 | (83) all_904_0 = all_898_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (77), (78) imply: % 74.61/10.98 | (84) all_901_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (84) implies: % 74.61/10.98 | (85) all_901_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (75), (83) imply: % 74.61/10.98 | (86) all_901_0 = all_898_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (86) implies: % 74.61/10.98 | (87) all_901_0 = all_898_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (76), (83) imply: % 74.61/10.98 | (88) all_898_0 = all_892_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (85), (87) imply: % 74.61/10.98 | (89) all_898_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (89) implies: % 74.61/10.98 | (90) all_898_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (88), (90) imply: % 74.61/10.98 | (91) all_892_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (91) implies: % 74.61/10.98 | (92) all_892_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (74), (92) imply: % 74.61/10.98 | (93) all_804_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (93) implies: % 74.61/10.98 | (94) all_804_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | COMBINE_EQS: (73), (94) imply: % 74.61/10.98 | (95) all_798_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | SIMP: (95) implies: % 74.61/10.98 | (96) all_798_0 = all_793_0 % 74.61/10.98 | % 74.61/10.98 | REDUCE: (38), (94) imply: % 74.61/10.98 | (97) gen_length$b(all_793_0) = size$ % 74.61/10.98 | % 74.61/10.98 | REDUCE: (64), (81) imply: % 74.61/10.98 | (98) fun_app$p(all_895_0, all_913_6) = all_913_5 % 74.61/10.98 | % 74.61/10.98 | REDUCE: (63), (81) imply: % 74.61/10.98 | (99) fun_app$p(all_895_0, all_913_14) = all_913_13 % 74.61/10.98 | % 74.61/10.98 | REDUCE: (34), (96) imply: % 74.61/10.98 | (100) Nat$(all_793_0) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (15) with all_913_10, all_795_0, 0, all_913_9, % 74.61/10.98 | simplifying with (30), (31), (54), (59) gives: % 74.61/10.98 | (101) ~ ($lesseq(0, all_913_9)) | ! [v0: Nat$] : ( ~ (fun_app$l(of_nat$, % 74.61/10.98 | v0) = $difference(-1, all_913_9)) | ~ Nat$(v0)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (16) with all_913_4, all_913_10, all_913_3, % 74.61/10.98 | all_913_9, simplifying with (54), (55), (59), (60) gives: % 74.61/10.98 | (102) $lesseq(0, all_913_9) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with nil$, nil$, all_795_0, all_795_0, % 74.61/10.98 | simplifying with (12), (32) gives: % 74.61/10.98 | (103) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(nil$, nil$) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.98 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_795_0) = % 74.61/10.98 | $difference(v2, v3) & fun_app$l(of_nat$, all_795_0) = v3 & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with all_913_13, all_913_13, all_913_12, % 74.61/10.98 | all_913_12, simplifying with (56), (61) gives: % 74.61/10.98 | (104) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(all_913_13, all_913_13) = v0 & fun_app$m(size$, v0) = v1 % 74.61/10.98 | & fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_12) = % 74.61/10.98 | $difference(v2, v3) & fun_app$l(of_nat$, all_913_12) = v3 & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with nil$, all_913_13, all_795_0, all_913_12, % 74.61/10.98 | simplifying with (12), (32), (56), (61) gives: % 74.61/10.98 | (105) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(nil$, all_913_13) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.98 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_12) = % 74.61/10.98 | $difference(v2, v3) & fun_app$l(of_nat$, all_795_0) = v3 & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with all_913_13, nil$, all_913_12, all_795_0, % 74.61/10.98 | simplifying with (12), (32), (56), (61) gives: % 74.61/10.98 | (106) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(all_913_13, nil$) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.98 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_12) = v3 & % 74.61/10.98 | fun_app$l(of_nat$, all_795_0) = $difference(v2, v3) & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with all_913_5, all_913_5, all_913_4, % 74.61/10.98 | all_913_4, simplifying with (57), (62) gives: % 74.61/10.98 | (107) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(all_913_5, all_913_5) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.98 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_4) = % 74.61/10.98 | $difference(v2, v3) & fun_app$l(of_nat$, all_913_4) = v3 & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.98 | GROUND_INST: instantiating (3) with all_913_13, all_913_5, all_913_12, % 74.61/10.98 | all_913_4, simplifying with (56), (57), (61), (62) gives: % 74.61/10.98 | (108) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.98 | : (splice$b(all_913_13, all_913_5) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.98 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_4) = % 74.61/10.98 | $difference(v2, v3) & fun_app$l(of_nat$, all_913_12) = v3 & % 74.61/10.98 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.98 | % 74.61/10.99 | GROUND_INST: instantiating (3) with all_913_5, all_913_13, all_913_4, % 74.61/10.99 | all_913_12, simplifying with (56), (57), (61), (62) gives: % 74.61/10.99 | (109) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.99 | : (splice$b(all_913_5, all_913_13) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.99 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_4) = v3 & % 74.61/10.99 | fun_app$l(of_nat$, all_913_12) = $difference(v2, v3) & % 74.61/10.99 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (3) with nil$, all_913_5, all_795_0, all_913_4, % 74.61/10.99 | simplifying with (12), (32), (57), (62) gives: % 74.61/10.99 | (110) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.99 | : (splice$b(nil$, all_913_5) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.99 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_4) = % 74.61/10.99 | $difference(v2, v3) & fun_app$l(of_nat$, all_795_0) = v3 & % 74.61/10.99 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (3) with all_913_5, nil$, all_913_4, all_795_0, % 74.61/10.99 | simplifying with (12), (32), (57), (62) gives: % 74.61/10.99 | (111) ? [v0: A_iarray_list$] : ? [v1: Nat$] : ? [v2: int] : ? [v3: int] % 74.61/10.99 | : (splice$b(all_913_5, nil$) = v0 & fun_app$m(size$, v0) = v1 & % 74.61/10.99 | fun_app$l(of_nat$, v1) = v2 & fun_app$l(of_nat$, all_913_4) = v3 & % 74.61/10.99 | fun_app$l(of_nat$, all_795_0) = $difference(v2, v3) & % 74.61/10.99 | A_iarray_list$(v0) & Nat$(v1)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (axiom28) with a$, all_913_8, simplifying with % 74.61/10.99 | (17), (71) gives: % 74.61/10.99 | (112) ? [v0: A_iarray_iarray$] : ? [v1: A_iarray_iarray$] : % 74.61/10.99 | (matrix_to_iarray$(all_913_8) = v0 & matrix_to_iarray$(a$) = v1 & % 74.61/10.99 | gauss_Jordan_iarrays$(v1) = v0 & A_iarray_iarray$(v1) & % 74.61/10.99 | A_iarray_iarray$(v0)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (2) with all_793_0, all_913_5, size$, all_913_4, % 74.61/10.99 | simplifying with (57), (62), (97), (100) gives: % 74.61/10.99 | (113) ? [v0: int] : ? [v1: int] : ? [v2: Nat$] : (fun_app$m(size$, % 74.61/10.99 | all_913_5) = v2 & fun_app$l(of_nat$, v2) = $difference(v0, v1) & % 74.61/10.99 | fun_app$l(of_nat$, all_913_4) = v0 & fun_app$l(of_nat$, all_793_0) % 74.61/10.99 | = v1 & Nat$(v2)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (2) with all_793_0, all_913_13, size$, all_913_12, % 74.61/10.99 | simplifying with (56), (61), (97), (100) gives: % 74.61/10.99 | (114) ? [v0: int] : ? [v1: int] : ? [v2: Nat$] : (fun_app$m(size$, % 74.61/10.99 | all_913_13) = v2 & fun_app$l(of_nat$, v2) = $difference(v0, v1) & % 74.61/10.99 | fun_app$l(of_nat$, all_913_12) = v0 & fun_app$l(of_nat$, all_793_0) % 74.61/10.99 | = v1 & Nat$(v2)) % 74.61/10.99 | % 74.61/10.99 | GROUND_INST: instantiating (2) with all_793_0, nil$, size$, all_795_0, % 74.61/10.99 | simplifying with (12), (32), (97), (100) gives: % 74.61/10.99 | (115) ? [v0: int] : ? [v1: int] : ? [v2: Nat$] : (fun_app$m(size$, nil$) % 74.61/10.99 | = v2 & fun_app$l(of_nat$, v2) = $difference(v0, v1) & % 74.61/10.99 | fun_app$l(of_nat$, all_795_0) = v0 & fun_app$l(of_nat$, all_793_0) % 74.61/10.99 | = v1 & Nat$(v2)) % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (115) with fresh symbols all_1000_0, all_1000_1, % 74.61/10.99 | all_1000_2 gives: % 74.61/10.99 | (116) fun_app$m(size$, nil$) = all_1000_0 & fun_app$l(of_nat$, all_1000_0) % 74.61/10.99 | = $difference(all_1000_2, all_1000_1) & fun_app$l(of_nat$, all_795_0) % 74.61/10.99 | = all_1000_2 & fun_app$l(of_nat$, all_793_0) = all_1000_1 & % 74.61/10.99 | Nat$(all_1000_0) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (116) implies: % 74.61/10.99 | (117) fun_app$l(of_nat$, all_795_0) = all_1000_2 % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (114) with fresh symbols all_1002_0, all_1002_1, % 74.61/10.99 | all_1002_2 gives: % 74.61/10.99 | (118) fun_app$m(size$, all_913_13) = all_1002_0 & fun_app$l(of_nat$, % 74.61/10.99 | all_1002_0) = $difference(all_1002_2, all_1002_1) & % 74.61/10.99 | fun_app$l(of_nat$, all_913_12) = all_1002_2 & fun_app$l(of_nat$, % 74.61/10.99 | all_793_0) = all_1002_1 & Nat$(all_1002_0) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (118) implies: % 74.61/10.99 | (119) fun_app$l(of_nat$, all_913_12) = all_1002_2 % 74.61/10.99 | (120) fun_app$m(size$, all_913_13) = all_1002_0 % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (113) with fresh symbols all_1004_0, all_1004_1, % 74.61/10.99 | all_1004_2 gives: % 74.61/10.99 | (121) fun_app$m(size$, all_913_5) = all_1004_0 & fun_app$l(of_nat$, % 74.61/10.99 | all_1004_0) = $difference(all_1004_2, all_1004_1) & % 74.61/10.99 | fun_app$l(of_nat$, all_913_4) = all_1004_2 & fun_app$l(of_nat$, % 74.61/10.99 | all_793_0) = all_1004_1 & Nat$(all_1004_0) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (121) implies: % 74.61/10.99 | (122) fun_app$l(of_nat$, all_913_4) = all_1004_2 % 74.61/10.99 | (123) fun_app$m(size$, all_913_5) = all_1004_0 % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (112) with fresh symbols all_1006_0, all_1006_1 gives: % 74.61/10.99 | (124) matrix_to_iarray$(all_913_8) = all_1006_1 & matrix_to_iarray$(a$) = % 74.61/10.99 | all_1006_0 & gauss_Jordan_iarrays$(all_1006_0) = all_1006_1 & % 74.61/10.99 | A_iarray_iarray$(all_1006_0) & A_iarray_iarray$(all_1006_1) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (124) implies: % 74.61/10.99 | (125) gauss_Jordan_iarrays$(all_1006_0) = all_1006_1 % 74.61/10.99 | (126) matrix_to_iarray$(a$) = all_1006_0 % 74.61/10.99 | (127) matrix_to_iarray$(all_913_8) = all_1006_1 % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (106) with fresh symbols all_1016_0, all_1016_1, % 74.61/10.99 | all_1016_2, all_1016_3 gives: % 74.61/10.99 | (128) splice$b(all_913_13, nil$) = all_1016_3 & fun_app$m(size$, % 74.61/10.99 | all_1016_3) = all_1016_2 & fun_app$l(of_nat$, all_1016_2) = % 74.61/10.99 | all_1016_1 & fun_app$l(of_nat$, all_913_12) = all_1016_0 & % 74.61/10.99 | fun_app$l(of_nat$, all_795_0) = $difference(all_1016_1, all_1016_0) & % 74.61/10.99 | A_iarray_list$(all_1016_3) & Nat$(all_1016_2) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (128) implies: % 74.61/10.99 | (129) fun_app$l(of_nat$, all_795_0) = $difference(all_1016_1, all_1016_0) % 74.61/10.99 | (130) fun_app$l(of_nat$, all_913_12) = all_1016_0 % 74.61/10.99 | % 74.61/10.99 | DELTA: instantiating (111) with fresh symbols all_1018_0, all_1018_1, % 74.61/10.99 | all_1018_2, all_1018_3 gives: % 74.61/10.99 | (131) splice$b(all_913_5, nil$) = all_1018_3 & fun_app$m(size$, all_1018_3) % 74.61/10.99 | = all_1018_2 & fun_app$l(of_nat$, all_1018_2) = all_1018_1 & % 74.61/10.99 | fun_app$l(of_nat$, all_913_4) = all_1018_0 & fun_app$l(of_nat$, % 74.61/10.99 | all_795_0) = $difference(all_1018_1, all_1018_0) & % 74.61/10.99 | A_iarray_list$(all_1018_3) & Nat$(all_1018_2) % 74.61/10.99 | % 74.61/10.99 | ALPHA: (131) implies: % 74.61/10.99 | (132) fun_app$l(of_nat$, all_795_0) = $difference(all_1018_1, all_1018_0) % 74.61/11.00 | (133) fun_app$l(of_nat$, all_913_4) = all_1018_0 % 74.61/11.00 | % 74.61/11.00 | DELTA: instantiating (110) with fresh symbols all_1020_0, all_1020_1, % 74.61/11.00 | all_1020_2, all_1020_3 gives: % 74.61/11.00 | (134) splice$b(nil$, all_913_5) = all_1020_3 & fun_app$m(size$, all_1020_3) % 74.61/11.00 | = all_1020_2 & fun_app$l(of_nat$, all_1020_2) = all_1020_1 & % 74.61/11.00 | fun_app$l(of_nat$, all_913_4) = $difference(all_1020_1, all_1020_0) & % 74.61/11.00 | fun_app$l(of_nat$, all_795_0) = all_1020_0 & % 74.61/11.00 | A_iarray_list$(all_1020_3) & Nat$(all_1020_2) % 74.61/11.00 | % 74.61/11.00 | ALPHA: (134) implies: % 74.61/11.00 | (135) fun_app$l(of_nat$, all_795_0) = all_1020_0 % 74.61/11.00 | (136) fun_app$l(of_nat$, all_913_4) = $difference(all_1020_1, all_1020_0) % 74.61/11.00 | % 74.61/11.00 | DELTA: instantiating (105) with fresh symbols all_1022_0, all_1022_1, % 74.61/11.00 | all_1022_2, all_1022_3 gives: % 74.61/11.00 | (137) splice$b(nil$, all_913_13) = all_1022_3 & fun_app$m(size$, % 74.61/11.00 | all_1022_3) = all_1022_2 & fun_app$l(of_nat$, all_1022_2) = % 74.61/11.00 | all_1022_1 & fun_app$l(of_nat$, all_913_12) = $difference(all_1022_1, % 74.61/11.00 | all_1022_0) & fun_app$l(of_nat$, all_795_0) = all_1022_0 & % 74.61/11.00 | A_iarray_list$(all_1022_3) & Nat$(all_1022_2) % 74.61/11.00 | % 74.61/11.00 | ALPHA: (137) implies: % 74.61/11.00 | (138) fun_app$l(of_nat$, all_795_0) = all_1022_0 % 74.61/11.00 | (139) fun_app$l(of_nat$, all_913_12) = $difference(all_1022_1, all_1022_0) % 74.61/11.00 | % 74.61/11.00 | DELTA: instantiating (103) with fresh symbols all_1024_0, all_1024_1, % 74.61/11.00 | all_1024_2, all_1024_3 gives: % 74.61/11.01 | (140) splice$b(nil$, nil$) = all_1024_3 & fun_app$m(size$, all_1024_3) = % 74.61/11.01 | all_1024_2 & fun_app$l(of_nat$, all_1024_2) = all_1024_1 & % 74.61/11.01 | fun_app$l(of_nat$, all_795_0) = $difference(all_1024_1, all_1024_0) & % 74.61/11.01 | fun_app$l(of_nat$, all_795_0) = all_1024_0 & % 74.61/11.01 | A_iarray_list$(all_1024_3) & Nat$(all_1024_2) % 74.61/11.01 | % 74.61/11.01 | ALPHA: (140) implies: % 74.61/11.01 | (141) fun_app$l(of_nat$, all_795_0) = all_1024_0 % 74.61/11.01 | (142) fun_app$l(of_nat$, all_795_0) = $difference(all_1024_1, all_1024_0) % 74.61/11.01 | % 74.61/11.01 | DELTA: instantiating (109) with fresh symbols all_1026_0, all_1026_1, % 74.61/11.01 | all_1026_2, all_1026_3 gives: % 74.61/11.01 | (143) splice$b(all_913_5, all_913_13) = all_1026_3 & fun_app$m(size$, % 75.02/11.01 | all_1026_3) = all_1026_2 & fun_app$l(of_nat$, all_1026_2) = % 75.02/11.01 | all_1026_1 & fun_app$l(of_nat$, all_913_4) = all_1026_0 & % 75.02/11.01 | fun_app$l(of_nat$, all_913_12) = $difference(all_1026_1, all_1026_0) % 75.02/11.01 | & A_iarray_list$(all_1026_3) & Nat$(all_1026_2) % 75.02/11.01 | % 75.02/11.01 | ALPHA: (143) implies: % 75.02/11.01 | (144) fun_app$l(of_nat$, all_913_12) = $difference(all_1026_1, all_1026_0) % 75.02/11.01 | (145) fun_app$l(of_nat$, all_913_4) = all_1026_0 % 75.02/11.01 | % 75.02/11.01 | DELTA: instantiating (107) with fresh symbols all_1028_0, all_1028_1, % 75.02/11.01 | all_1028_2, all_1028_3 gives: % 75.02/11.01 | (146) splice$b(all_913_5, all_913_5) = all_1028_3 & fun_app$m(size$, % 75.02/11.01 | all_1028_3) = all_1028_2 & fun_app$l(of_nat$, all_1028_2) = % 75.02/11.01 | all_1028_1 & fun_app$l(of_nat$, all_913_4) = $difference(all_1028_1, % 75.02/11.01 | all_1028_0) & fun_app$l(of_nat$, all_913_4) = all_1028_0 & % 75.02/11.01 | A_iarray_list$(all_1028_3) & Nat$(all_1028_2) % 75.02/11.01 | % 75.02/11.01 | ALPHA: (146) implies: % 75.02/11.01 | (147) fun_app$l(of_nat$, all_913_4) = all_1028_0 % 75.02/11.01 | (148) fun_app$l(of_nat$, all_913_4) = $difference(all_1028_1, all_1028_0) % 75.02/11.01 | % 75.02/11.01 | DELTA: instantiating (104) with fresh symbols all_1030_0, all_1030_1, % 75.02/11.01 | all_1030_2, all_1030_3 gives: % 75.02/11.01 | (149) splice$b(all_913_13, all_913_13) = all_1030_3 & fun_app$m(size$, % 75.02/11.01 | all_1030_3) = all_1030_2 & fun_app$l(of_nat$, all_1030_2) = % 75.02/11.01 | all_1030_1 & fun_app$l(of_nat$, all_913_12) = $difference(all_1030_1, % 75.02/11.01 | all_1030_0) & fun_app$l(of_nat$, all_913_12) = all_1030_0 & % 75.02/11.01 | A_iarray_list$(all_1030_3) & Nat$(all_1030_2) % 75.02/11.01 | % 75.02/11.01 | ALPHA: (149) implies: % 75.02/11.01 | (150) fun_app$l(of_nat$, all_913_12) = all_1030_0 % 75.02/11.01 | (151) fun_app$l(of_nat$, all_913_12) = $difference(all_1030_1, all_1030_0) % 75.02/11.01 | % 75.02/11.01 | DELTA: instantiating (108) with fresh symbols all_1032_0, all_1032_1, % 75.02/11.01 | all_1032_2, all_1032_3 gives: % 75.02/11.01 | (152) splice$b(all_913_13, all_913_5) = all_1032_3 & fun_app$m(size$, % 75.02/11.01 | all_1032_3) = all_1032_2 & fun_app$l(of_nat$, all_1032_2) = % 75.02/11.01 | all_1032_1 & fun_app$l(of_nat$, all_913_4) = $difference(all_1032_1, % 75.02/11.01 | all_1032_0) & fun_app$l(of_nat$, all_913_12) = all_1032_0 & % 75.02/11.01 | A_iarray_list$(all_1032_3) & Nat$(all_1032_2) % 75.02/11.01 | % 75.02/11.01 | ALPHA: (152) implies: % 75.02/11.01 | (153) fun_app$l(of_nat$, all_913_12) = all_1032_0 % 75.02/11.01 | (154) fun_app$l(of_nat$, all_913_4) = $difference(all_1032_1, all_1032_0) % 75.02/11.01 | % 75.02/11.01 | BETA: splitting (101) gives: % 75.02/11.01 | % 75.02/11.02 | Case 1: % 75.02/11.02 | | % 75.02/11.02 | | (155) $lesseq(all_913_9, -1) % 75.02/11.02 | | % 75.02/11.02 | | COMBINE_INEQS: (102), (155) imply: % 75.02/11.02 | | (156) $false % 75.02/11.02 | | % 75.02/11.02 | | CLOSE: (156) is inconsistent. % 75.02/11.02 | | % 75.02/11.02 | Case 2: % 75.02/11.02 | | % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1016_1, all_1016_0), % 75.02/11.02 | | all_1020_0, all_795_0, of_nat$, simplifying with (129), (135) % 75.02/11.02 | | gives: % 75.02/11.02 | | (157) $sum(all_1020_0, all_1016_0) = all_1016_1 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1022_0, all_1024_0, all_795_0, % 75.02/11.02 | | of_nat$, simplifying with (138), (141) gives: % 75.02/11.02 | | (158) all_1024_0 = all_1022_0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1020_0, all_1024_0, all_795_0, % 75.02/11.02 | | of_nat$, simplifying with (135), (141) gives: % 75.02/11.02 | | (159) all_1024_0 = all_1020_0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1018_1, all_1018_0), % 75.02/11.02 | | all_1024_0, all_795_0, of_nat$, simplifying with (132), (141) % 75.02/11.02 | | gives: % 75.02/11.02 | | (160) $sum(all_1024_0, all_1018_0) = all_1018_1 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1022_0, $difference(all_1024_1, % 75.02/11.02 | | all_1024_0), all_795_0, of_nat$, simplifying with (138), % 75.02/11.02 | | (142) gives: % 75.02/11.02 | | (161) $sum($difference(all_1024_0, all_1024_1), all_1022_0) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1000_2, $difference(all_1024_1, % 75.02/11.02 | | all_1024_0), all_795_0, of_nat$, simplifying with (117), % 75.02/11.02 | | (142) gives: % 75.02/11.02 | | (162) $sum($difference(all_1024_0, all_1024_1), all_1000_2) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1016_0, $difference(all_1022_1, % 75.02/11.02 | | all_1022_0), all_913_12, of_nat$, simplifying with (130), % 75.02/11.02 | | (139) gives: % 75.02/11.02 | | (163) $sum($difference(all_1022_0, all_1022_1), all_1016_0) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1022_1, all_1022_0), % 75.02/11.02 | | all_1030_0, all_913_12, of_nat$, simplifying with (139), (150) % 75.02/11.02 | | gives: % 75.02/11.02 | | (164) $sum(all_1030_0, all_1022_0) = all_1022_1 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_913_11, all_1030_0, all_913_12, % 75.02/11.02 | | of_nat$, simplifying with (58), (150) gives: % 75.02/11.02 | | (165) all_1030_0 = all_913_11 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1026_1, all_1026_0), % 75.02/11.02 | | $difference(all_1030_1, all_1030_0), all_913_12, of_nat$, % 75.02/11.02 | | simplifying with (144), (151) gives: % 75.02/11.02 | | (166) $sum($difference($difference(all_1030_0, all_1030_1), all_1026_0), % 75.02/11.02 | | all_1026_1) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1016_0, $difference(all_1030_1, % 75.02/11.02 | | all_1030_0), all_913_12, of_nat$, simplifying with (130), % 75.02/11.02 | | (151) gives: % 75.02/11.02 | | (167) $sum($difference(all_1030_0, all_1030_1), all_1016_0) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1030_1, all_1030_0), % 75.02/11.02 | | all_1032_0, all_913_12, of_nat$, simplifying with (151), (153) % 75.02/11.02 | | gives: % 75.02/11.02 | | (168) $sum(all_1032_0, all_1030_0) = all_1030_1 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1002_2, all_1032_0, all_913_12, % 75.02/11.02 | | of_nat$, simplifying with (119), (153) gives: % 75.02/11.02 | | (169) all_1032_0 = all_1002_2 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1020_1, all_1020_0), % 75.02/11.02 | | all_1026_0, all_913_4, of_nat$, simplifying with (136), (145) % 75.02/11.02 | | gives: % 75.02/11.02 | | (170) $sum(all_1026_0, all_1020_0) = all_1020_1 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1026_0, all_1028_0, all_913_4, % 75.02/11.02 | | of_nat$, simplifying with (145), (147) gives: % 75.02/11.02 | | (171) all_1028_0 = all_1026_0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with $difference(all_1020_1, all_1020_0), % 75.02/11.02 | | $difference(all_1028_1, all_1028_0), all_913_4, of_nat$, % 75.02/11.02 | | simplifying with (136), (148) gives: % 75.02/11.02 | | (172) $sum($difference($difference(all_1028_0, all_1028_1), all_1020_0), % 75.02/11.02 | | all_1020_1) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_1018_0, $difference(all_1028_1, % 75.02/11.02 | | all_1028_0), all_913_4, of_nat$, simplifying with (133), % 75.02/11.02 | | (148) gives: % 75.02/11.02 | | (173) $sum($difference(all_1028_0, all_1028_1), all_1018_0) = 0 % 75.02/11.02 | | % 75.02/11.02 | | GROUND_INST: instantiating (24) with all_913_3, $difference(all_1028_1, % 75.02/11.02 | | all_1028_0), all_913_4, of_nat$, simplifying with (60), (148) % 75.02/11.02 | | gives: % 75.02/11.02 | | (174) $sum($difference(all_1028_0, all_1028_1), all_913_3) = 0 % 75.02/11.02 | | % 75.02/11.03 | | GROUND_INST: instantiating (24) with all_1028_0, $difference(all_1032_1, % 75.02/11.03 | | all_1032_0), all_913_4, of_nat$, simplifying with (147), % 75.02/11.03 | | (154) gives: % 75.02/11.03 | | (175) $sum($difference(all_1032_0, all_1032_1), all_1028_0) = 0 % 75.02/11.03 | | % 75.02/11.03 | | GROUND_INST: instantiating (24) with all_1004_2, $difference(all_1032_1, % 75.02/11.03 | | all_1032_0), all_913_4, of_nat$, simplifying with (122), % 75.02/11.03 | | (154) gives: % 75.02/11.03 | | (176) $sum($difference(all_1032_0, all_1032_1), all_1004_2) = 0 % 75.02/11.03 | | % 75.02/11.03 | | GROUND_INST: instantiating (25) with all_913_12, all_1002_0, all_913_13, % 75.02/11.03 | | size$, simplifying with (61), (120) gives: % 75.02/11.03 | | (177) all_1002_0 = all_913_12 % 75.02/11.03 | | % 75.02/11.03 | | GROUND_INST: instantiating (25) with all_913_4, all_1004_0, all_913_5, % 75.02/11.03 | | size$, simplifying with (62), (123) gives: % 75.02/11.03 | | (178) all_1004_0 = all_913_4 % 75.02/11.03 | | % 75.02/11.03 | | GROUND_INST: instantiating (22) with all_913_16, all_1006_0, a$, simplifying % 75.02/11.03 | | with (69), (126) gives: % 75.02/11.03 | | (179) all_1006_0 = all_913_16 % 75.02/11.03 | | % 75.02/11.03 | | GROUND_INST: instantiating (22) with all_913_7, all_1006_1, all_913_8, % 75.02/11.03 | | simplifying with (70), (127) gives: % 75.02/11.03 | | (180) all_1006_1 = all_913_7 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (169), (176) imply: % 75.02/11.03 | | (181) $difference(all_1032_1, all_1004_2) = all_1002_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (168), (176) imply: % 75.02/11.03 | | (182) $difference($sum(all_1032_1, all_1030_0), all_1030_1) = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (175), (176) imply: % 75.02/11.03 | | (183) all_1028_0 = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (181), (182) imply: % 75.02/11.03 | | (184) $sum($difference(all_1030_0, all_1030_1), all_1002_2) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (165), (166) imply: % 75.02/11.03 | | (185) $difference($sum(all_1030_1, all_1026_0), all_1026_1) = all_913_11 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (166), (184) imply: % 75.02/11.03 | | (186) $sum($difference(all_1026_0, all_1026_1), all_1002_2) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (166), (167) imply: % 75.02/11.03 | | (187) $sum($difference(all_1026_0, all_1026_1), all_1016_0) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (164), (166) imply: % 75.02/11.03 | | (188) $sum($difference($sum(all_1030_1, all_1026_0), all_1026_1), % 75.02/11.03 | | all_1022_0) = all_1022_1 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (185), (188) imply: % 75.02/11.03 | | (189) $sum($difference(all_1022_0, all_1022_1), all_913_11) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (173), (183) imply: % 75.02/11.03 | | (190) $difference(all_1028_1, all_1018_0) = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | SIMP: (190) implies: % 75.02/11.03 | | (191) $difference(all_1028_1, all_1018_0) = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (172), (183) imply: % 75.02/11.03 | | (192) $difference($sum(all_1028_1, all_1020_0), all_1020_1) = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | SIMP: (192) implies: % 75.02/11.03 | | (193) $difference($sum(all_1028_1, all_1020_0), all_1020_1) = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (171), (183) imply: % 75.02/11.03 | | (194) all_1026_0 = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | SIMP: (194) implies: % 75.02/11.03 | | (195) all_1026_0 = all_1004_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (174), (183) imply: % 75.02/11.03 | | (196) $difference(all_1028_1, all_1004_2) = all_913_3 % 75.02/11.03 | | % 75.02/11.03 | | SIMP: (196) implies: % 75.02/11.03 | | (197) $difference(all_1028_1, all_1004_2) = all_913_3 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (191), (193) imply: % 75.02/11.03 | | (198) $sum($difference(all_1020_0, all_1020_1), all_1018_0) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (191), (197) imply: % 75.02/11.03 | | (199) all_1018_0 = all_913_3 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (186), (195) imply: % 75.02/11.03 | | (200) $difference(all_1026_1, all_1004_2) = all_1002_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (170), (186) imply: % 75.02/11.03 | | (201) $difference($sum(all_1026_1, all_1020_0), all_1020_1) = all_1002_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (186), (187) imply: % 75.02/11.03 | | (202) all_1016_0 = all_1002_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (200), (201) imply: % 75.02/11.03 | | (203) $sum($difference(all_1020_0, all_1020_1), all_1004_2) = 0 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (161), (162) imply: % 75.02/11.03 | | (204) all_1022_0 = all_1000_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (160), (162) imply: % 75.02/11.03 | | (205) $difference($sum(all_1024_1, all_1018_0), all_1018_1) = all_1000_2 % 75.02/11.03 | | % 75.02/11.03 | | COMBINE_EQS: (158), (162) imply: % 75.02/11.03 | | (206) $difference(all_1024_1, all_1022_0) = all_1000_2 % 75.02/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (159), (162) imply: % 75.11/11.03 | | (207) $difference(all_1024_1, all_1020_0) = all_1000_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (205), (206) imply: % 75.11/11.03 | | (208) $sum(all_1022_0, all_1018_0) = all_1018_1 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (208) implies: % 75.11/11.03 | | (209) $sum(all_1022_0, all_1018_0) = all_1018_1 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (205), (207) imply: % 75.11/11.03 | | (210) $sum(all_1020_0, all_1018_0) = all_1018_1 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (210) implies: % 75.11/11.03 | | (211) $sum(all_1020_0, all_1018_0) = all_1018_1 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (163), (204) imply: % 75.11/11.03 | | (212) $difference(all_1022_1, all_1016_0) = all_1000_2 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (212) implies: % 75.11/11.03 | | (213) $difference(all_1022_1, all_1016_0) = all_1000_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (204), (209) imply: % 75.11/11.03 | | (214) $sum($difference(all_1018_0, all_1018_1), all_1000_2) = 0 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (189), (204) imply: % 75.11/11.03 | | (215) $difference(all_1022_1, all_1000_2) = all_913_11 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (215) implies: % 75.11/11.03 | | (216) $difference(all_1022_1, all_1000_2) = all_913_11 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (213), (216) imply: % 75.11/11.03 | | (217) all_1016_0 = all_913_11 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (217) implies: % 75.11/11.03 | | (218) all_1016_0 = all_913_11 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (157), (203) imply: % 75.11/11.03 | | (219) $difference($sum(all_1020_1, all_1016_0), all_1016_1) = all_1004_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (198), (203) imply: % 75.11/11.03 | | (220) all_1018_0 = all_1004_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (203), (211) imply: % 75.11/11.03 | | (221) $difference($sum(all_1020_1, all_1018_0), all_1018_1) = all_1004_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (219), (221) imply: % 75.11/11.03 | | (222) $sum($difference($difference(all_1018_0, all_1018_1), all_1016_0), % 75.11/11.03 | | all_1016_1) = 0 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (220), (222) imply: % 75.11/11.03 | | (223) $difference($sum(all_1018_1, all_1016_0), all_1016_1) = all_1004_2 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (223) implies: % 75.11/11.03 | | (224) $difference($sum(all_1018_1, all_1016_0), all_1016_1) = all_1004_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (214), (220) imply: % 75.11/11.03 | | (225) $difference(all_1018_1, all_1004_2) = all_1000_2 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (225) implies: % 75.11/11.03 | | (226) $difference(all_1018_1, all_1004_2) = all_1000_2 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (199), (220) imply: % 75.11/11.03 | | (227) all_1004_2 = all_913_3 % 75.11/11.03 | | % 75.11/11.03 | | COMBINE_EQS: (224), (226) imply: % 75.11/11.03 | | (228) $sum($difference(all_1016_0, all_1016_1), all_1000_2) = 0 % 75.11/11.03 | | % 75.11/11.03 | | SIMP: (228) implies: % 75.11/11.03 | | (229) $sum($difference(all_1016_0, all_1016_1), all_1000_2) = 0 % 75.11/11.03 | | % 75.11/11.04 | | COMBINE_EQS: (202), (229) imply: % 75.11/11.04 | | (230) $difference(all_1016_1, all_1002_2) = all_1000_2 % 75.11/11.04 | | % 75.11/11.04 | | COMBINE_EQS: (218), (229) imply: % 75.11/11.04 | | (231) $difference(all_1016_1, all_1000_2) = all_913_11 % 75.11/11.04 | | % 75.11/11.04 | | COMBINE_EQS: (230), (231) imply: % 75.11/11.04 | | (232) all_1002_2 = all_913_11 % 75.11/11.04 | | % 75.11/11.04 | | SIMP: (232) implies: % 75.11/11.04 | | (233) all_1002_2 = all_913_11 % 75.11/11.04 | | % 75.11/11.04 | | REDUCE: (125), (179), (180) imply: % 75.11/11.04 | | (234) gauss_Jordan_iarrays$(all_913_16) = all_913_7 % 75.11/11.04 | | % 75.11/11.04 | | GROUND_INST: instantiating (20) with all_913_15, all_913_7, all_913_16, % 75.11/11.04 | | simplifying with (67), (234) gives: % 75.11/11.04 | | (235) all_913_7 = all_913_15 % 75.11/11.04 | | % 75.11/11.04 | | REDUCE: (66), (235) imply: % 75.11/11.04 | | (236) list_of$(all_913_15) = all_913_6 % 75.11/11.04 | | % 75.11/11.04 | | GROUND_INST: instantiating (19) with all_913_14, all_913_6, all_913_15, % 75.11/11.04 | | simplifying with (65), (236) gives: % 75.11/11.04 | | (237) all_913_6 = all_913_14 % 75.11/11.04 | | % 75.11/11.04 | | REDUCE: (98), (237) imply: % 75.11/11.04 | | (238) fun_app$p(all_895_0, all_913_14) = all_913_5 % 75.11/11.04 | | % 75.11/11.04 | | GROUND_INST: instantiating (26) with all_913_13, all_913_5, all_913_14, % 75.11/11.04 | | all_895_0, simplifying with (99), (238) gives: % 75.11/11.04 | | (239) all_913_5 = all_913_13 % 75.11/11.04 | | % 75.11/11.04 | | REDUCE: (62), (239) imply: % 75.11/11.04 | | (240) fun_app$m(size$, all_913_13) = all_913_4 % 75.11/11.04 | | % 75.11/11.04 | | GROUND_INST: instantiating (25) with all_913_12, all_913_4, all_913_13, % 75.11/11.04 | | size$, simplifying with (61), (240) gives: % 75.11/11.04 | | (241) all_913_4 = all_913_12 % 75.11/11.04 | | % 75.11/11.04 | | REDUCE: (60), (241) imply: % 75.11/11.04 | | (242) fun_app$l(of_nat$, all_913_12) = all_913_3 % 75.11/11.04 | | % 75.11/11.04 | | GROUND_INST: instantiating (24) with all_913_11, all_913_3, all_913_12, % 75.11/11.04 | | of_nat$, simplifying with (58), (242) gives: % 75.11/11.04 | | (243) all_913_3 = all_913_11 % 75.11/11.04 | | % 75.11/11.04 | | BETA: splitting (72) gives: % 75.11/11.04 | | % 75.11/11.04 | | Case 1: % 75.11/11.04 | | | % 75.11/11.04 | | | (244) all_913_3 = all_913_9 & ~ (all_913_0 = none$) & ~ (all_913_9 = % 75.11/11.04 | | | all_913_11) % 75.11/11.04 | | | % 75.11/11.04 | | | ALPHA: (244) implies: % 75.11/11.04 | | | (245) all_913_3 = all_913_9 % 75.11/11.04 | | | (246) ~ (all_913_9 = all_913_11) % 75.11/11.04 | | | % 75.11/11.04 | | | COMBINE_EQS: (243), (245) imply: % 75.11/11.04 | | | (247) all_913_9 = all_913_11 % 75.11/11.04 | | | % 75.11/11.04 | | | REDUCE: (246), (247) imply: % 75.11/11.04 | | | (248) $false % 75.11/11.04 | | | % 75.11/11.04 | | | CLOSE: (248) is inconsistent. % 75.11/11.04 | | | % 75.11/11.04 | | Case 2: % 75.11/11.04 | | | % 75.11/11.04 | | | (249) all_913_9 = all_913_11 & ~ (all_913_0 = none$) & ~ (all_913_3 = % 75.11/11.04 | | | all_913_11) % 75.11/11.04 | | | % 75.11/11.04 | | | ALPHA: (249) implies: % 75.11/11.04 | | | (250) ~ (all_913_3 = all_913_11) % 75.11/11.04 | | | % 75.11/11.04 | | | REDUCE: (243), (250) imply: % 75.11/11.04 | | | (251) $false % 75.11/11.04 | | | % 75.11/11.04 | | | CLOSE: (251) is inconsistent. % 75.11/11.04 | | | % 75.11/11.04 | | End of split % 75.11/11.04 | | % 75.11/11.04 | End of split % 75.11/11.04 | % 75.11/11.04 End of proof % 75.11/11.04 % SZS output end Proof for theBenchmark % 75.11/11.04 % 75.11/11.04 10359ms %------------------------------------------------------------------------------