%------------------------------------------------------------------------------ % 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 : n014.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 93.36s 12.96s % Output : Proof 225.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 15:45:01 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.62 Running up to 7 provers in parallel. % 0.20/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.73/1.06 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.06 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.06 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.06 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.06 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.07 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 2.73/1.07 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 14.56/2.71 Prover 5: Preprocessing ... % 14.56/2.71 Prover 6: Preprocessing ... % 14.56/2.75 Prover 0: Preprocessing ... % 14.56/2.76 Prover 1: Preprocessing ... % 14.56/2.76 Prover 2: Preprocessing ... % 14.56/2.78 Prover 3: Preprocessing ... % 14.56/2.79 Prover 4: Preprocessing ... % 33.98/5.28 Prover 1: Warning: ignoring some quantifiers % 34.75/5.36 Prover 3: Warning: ignoring some quantifiers % 35.30/5.42 Prover 6: Proving ... % 35.30/5.44 Prover 3: Constructing countermodel ... % 35.84/5.49 Prover 1: Constructing countermodel ... % 39.73/6.00 Prover 4: Warning: ignoring some quantifiers % 40.22/6.09 Prover 5: Proving ... % 41.20/6.22 Prover 4: Constructing countermodel ... % 41.86/6.33 Prover 0: Proving ... % 43.31/6.46 Prover 2: Proving ... % 88.67/12.33 Prover 2: stopped % 88.67/12.34 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 88.67/12.35 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 93.36/12.95 Prover 3: proved (12319ms) % 93.36/12.95 % 93.36/12.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 93.36/12.96 % 93.36/12.96 Prover 5: stopped % 93.36/12.96 Prover 6: stopped % 93.36/12.97 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 93.36/12.97 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 93.36/12.97 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 93.36/12.98 Prover 0: stopped % 93.36/12.98 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 93.36/12.98 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 93.36/12.99 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 93.36/12.99 Prover 13: Warning: Problem contains reals, using incomplete axiomatisation % 93.36/13.00 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 94.13/13.06 Prover 7: Preprocessing ... % 98.66/13.75 Prover 8: Preprocessing ... % 98.66/13.78 Prover 10: Preprocessing ... % 98.66/13.79 Prover 11: Preprocessing ... % 99.42/13.89 Prover 13: Preprocessing ... % 103.25/14.30 Prover 7: Warning: ignoring some quantifiers % 103.96/14.37 Prover 7: Constructing countermodel ... % 105.47/14.66 Prover 8: Warning: ignoring some quantifiers % 107.04/14.72 Prover 8: Constructing countermodel ... % 107.85/14.82 Prover 10: Warning: ignoring some quantifiers % 107.85/14.87 Prover 10: Constructing countermodel ... % 109.52/15.13 Prover 11: Warning: ignoring some quantifiers % 110.33/15.27 Prover 11: Constructing countermodel ... % 112.18/15.38 Prover 13: Warning: ignoring some quantifiers % 113.27/15.54 Prover 13: Constructing countermodel ... % 116.31/15.98 Prover 1: stopped % 116.31/15.98 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 116.31/15.99 Prover 16: Warning: Problem contains reals, using incomplete axiomatisation % 120.89/16.60 Prover 16: Preprocessing ... % 124.02/16.99 Prover 13: stopped % 124.70/17.00 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 124.70/17.02 Prover 19: Warning: Problem contains reals, using incomplete axiomatisation % 128.06/17.51 Prover 19: Preprocessing ... % 128.72/17.52 Prover 16: Warning: ignoring some quantifiers % 129.19/17.60 Prover 16: Constructing countermodel ... % 139.36/18.90 Prover 19: Warning: ignoring some quantifiers % 140.04/18.99 Prover 19: Constructing countermodel ... % 153.21/20.77 Prover 16: stopped % 170.82/23.12 Prover 19: stopped % 201.32/27.97 Prover 4: stopped % 219.00/31.87 Prover 7: stopped % 223.89/33.15 Prover 8: Found proof (size 154) % 223.89/33.15 Prover 8: proved (20150ms) % 223.89/33.16 Prover 11: stopped % 223.89/33.16 Prover 10: stopped % 223.89/33.16 % 223.89/33.16 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 223.89/33.16 % 224.14/33.18 % SZS output start Proof for theBenchmark % 224.14/33.21 Assumptions after simplification: % 224.14/33.21 --------------------------------- % 224.14/33.21 % 224.14/33.21 (axiom10) % 224.14/33.24 Nat_int_fun$(of_nat$) & A_rows_vec$(zero$) & A_n_vec_set_bool_fun$(finite$) & % 224.14/33.24 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & ? [v0: % 224.14/33.24 A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.14/33.24 A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.14/33.24 A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.14/33.24 A_n_vec_rows_vec$(v1) | ? [v3: Nat$] : ? [v4: int] : ? [v5: any] : % 224.14/33.24 (fun_app$k(v0, v2) = v3 & fun_app$j(of_nat$, v3) = v4 & fun_app$d(finite$, % 224.14/33.24 v2) = v5 & Nat$(v3) & ( ~ (v5 = 0) | ~ ($lesseq(1, v4)))))) % 224.14/33.24 % 224.14/33.24 (axiom102) % 224.14/33.24 Nat_int_fun$(of_nat$) & A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & % 224.14/33.24 A_n_vec_set$(bot$a) & ? [v0: A_n_vec_set_nat_fun$] : ? [v1: Nat$] : % 224.14/33.24 (dim$(vector_scalar_mult$) = v0 & fun_app$k(v0, bot$a) = v1 & % 224.14/33.24 fun_app$j(of_nat$, v1) = 0 & A_n_vec_set_nat_fun$(v0) & Nat$(v1)) % 224.14/33.24 % 224.14/33.24 (axiom12) % 224.46/33.25 Nat_int_fun$(of_nat$) & A_rows_vec$(zero$) & A_n_vec_set_bool_fun$(finite$) & % 224.46/33.25 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & ? [v0: % 224.46/33.25 A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.46/33.25 A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.46/33.25 A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.46/33.25 A_n_vec_rows_vec$(v1) | ? [v3: any] : ? [v4: Nat$] : ? [v5: int] : % 224.46/33.25 (fun_app$k(v0, v2) = v4 & fun_app$j(of_nat$, v4) = v5 & fun_app$d(finite$, % 224.46/33.25 v2) = v3 & Nat$(v4) & (v3 = 0 | ~ ($lesseq(v5, 0))))) % 224.46/33.25 % 224.46/33.25 (axiom150) % 224.46/33.25 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.25 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.25 % 224.46/33.25 (axiom177) % 224.46/33.25 fun_app$j(of_nat$, bot$g) = 0 & Nat_int_fun$(of_nat$) & Nat$(bot$g) % 224.46/33.25 % 224.46/33.25 (axiom216) % 224.46/33.25 Nat$(bot$g) & Nat_nat_bool_fun_fun$(less$) & ! [v0: Nat$] : ! [v1: % 224.46/33.25 Nat_bool_fun$] : ( ~ (fun_app$q(less$, v0) = v1) | ~ Nat$(v0) | ? [v2: % 224.46/33.25 int] : ( ~ (v2 = 0) & fun_app$g(v1, bot$g) = v2)) % 224.46/33.25 % 224.46/33.25 (axiom264) % 224.46/33.25 Nat_int_fun$(of_nat$) & A_n_vec$(zero$a) & % 224.46/33.25 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & A_n_vec_set$(bot$a) & ? % 224.46/33.25 [v0: A_n_vec_set_nat_fun$] : ? [v1: A_n_vec_set$] : (insert$a(zero$a, bot$a) % 224.46/33.25 = v1 & dim$(vector_scalar_mult$) = v0 & A_n_vec_set_nat_fun$(v0) & % 224.46/33.25 A_n_vec_set$(v1) & ! [v2: A_n_vec_set$] : ! [v3: Nat$] : (v2 = v1 | v2 = % 224.46/33.25 bot$a | ~ (fun_app$k(v0, v2) = v3) | ~ A_n_vec_set$(v2) | ? [v4: int] : % 224.46/33.25 ( ~ (v4 = 0) & fun_app$j(of_nat$, v3) = v4))) % 224.46/33.25 % 224.46/33.25 (axiom27) % 224.46/33.25 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.25 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.25 % 224.46/33.25 (axiom271) % 224.46/33.26 Nat_int_fun$(of_nat$) & A_n_vec$(zero$a) & % 224.46/33.26 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & A_n_vec_set$(bot$a) & ? % 224.46/33.26 [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.46/33.26 A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec$] : ! [v2: A_n_vec_set$] : (v1 = % 224.46/33.26 zero$a | ~ (insert$a(v1, bot$a) = v2) | ~ A_n_vec$(v1) | ? [v3: Nat$] : % 224.46/33.26 (fun_app$k(v0, v2) = v3 & fun_app$j(of_nat$, v3) = 1 & Nat$(v3))) & ! % 224.46/33.26 [v1: A_n_vec_set$] : ( ~ (insert$a(zero$a, bot$a) = v1) | ? [v2: Nat$] : % 224.46/33.26 (fun_app$k(v0, v1) = v2 & fun_app$j(of_nat$, v2) = 0 & Nat$(v2)))) % 224.46/33.26 % 224.46/33.26 (axiom28) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom280) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom29) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom313) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom36) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat_bool_fun$] : ! [v1: Nat$] : ! [v2: int] % 224.46/33.26 : (v2 = 0 | ~ (fun_app$g(v0, v1) = v2) | ~ Nat_bool_fun$(v0) | ~ Nat$(v1) | % 224.46/33.26 ? [v3: Nat$] : ? [v4: int] : ? [v5: int] : ( ~ (v4 = 0) & % 224.46/33.26 fun_app$j(of_nat$, v3) = v5 & fun_app$g(v0, v3) = v4 & Nat$(v3) & ! [v6: % 224.46/33.26 Nat$] : ! [v7: int] : ( ~ ($lesseq(1, $difference(v5, v7))) | ~ % 224.46/33.26 (fun_app$j(of_nat$, v6) = v7) | ~ Nat$(v6) | fun_app$g(v0, v6) = 0))) % 224.46/33.26 % 224.46/33.26 (axiom391) % 224.46/33.26 Nat$(bot$g) & Nat_nat_bool_fun_fun$(less_eq$c) & ? [v0: Nat_bool_fun$] : % 224.46/33.26 (fun_app$q(less_eq$c, bot$g) = v0 & Nat_bool_fun$(v0) & ! [v1: Nat$] : ! % 224.46/33.26 [v2: int] : (v2 = 0 | ~ (fun_app$g(v0, v1) = v2) | ~ Nat$(v1))) % 224.46/33.26 % 224.46/33.26 (axiom478) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom49) % 224.46/33.26 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.26 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.26 % 224.46/33.26 (axiom50) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom51) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom52) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom524) % 224.46/33.27 Nat$(zero$c) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat$] : ! [v3: % 224.46/33.27 Nat_nat_fun$] : ! [v4: Nat$] : ! [v5: Nat_nat_fun$] : ! [v6: Nat$] : (v6 % 224.46/33.27 = v4 | ~ (times$b(v2) = v5) | ~ (times$b(v0) = v3) | ~ (fun_app$r(v5, v1) % 224.46/33.27 = v6) | ~ (fun_app$r(v3, v1) = v4) | ~ Nat$(v2) | ~ Nat$(v1) | ~ % 224.46/33.27 Nat$(v0) | ( ~ (v2 = v0) & ~ (v1 = zero$c))) & ! [v0: Nat$] : ! [v1: % 224.46/33.27 Nat$] : ! [v2: Nat$] : ! [v3: Nat_nat_fun$] : ! [v4: Nat$] : ! [v5: % 224.46/33.27 Nat_nat_fun$] : (v2 = v0 | v1 = zero$c | ~ (times$b(v2) = v5) | ~ % 224.46/33.27 (times$b(v0) = v3) | ~ (fun_app$r(v5, v1) = v4) | ~ (fun_app$r(v3, v1) = % 224.46/33.27 v4) | ~ Nat$(v2) | ~ Nat$(v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom53) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom545) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom546) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom56) % 224.46/33.27 Nat$(zero$c) & Nat_nat_bool_fun_fun$(less$) & ? [v0: Nat_bool_fun$] : % 224.46/33.27 (fun_app$q(less$, zero$c) = v0 & Nat_bool_fun$(v0) & ~ (fun_app$g(v0, zero$c) % 224.46/33.27 = 0) & ! [v1: Nat$] : ! [v2: int] : (v2 = 0 | v1 = zero$c | ~ % 224.46/33.27 (fun_app$g(v0, v1) = v2) | ~ Nat$(v1))) % 224.46/33.27 % 224.46/33.27 (axiom599) % 224.46/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.46/33.27 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.46/33.27 % 224.46/33.27 (axiom60) % 224.46/33.27 Nat_int_fun$(of_nat$) & A_rows_vec$(zero$) & % 224.46/33.27 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & ? [v0: % 224.46/33.27 A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.46/33.27 A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.46/33.27 A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.46/33.27 A_n_vec_rows_vec$(v1) | ? [v3: Nat$] : ? [v4: int] : ? [v5: % 224.46/33.27 A_n_vec_set$] : ? [v6: Nat$] : (null_space$a(v1) = v5 & fun_app$k(v0, % 224.46/33.27 v5) = v6 & fun_app$k(v0, v2) = v3 & fun_app$j(of_nat$, v6) = v4 & % 224.46/33.27 fun_app$j(of_nat$, v3) = v4 & Nat$(v6) & Nat$(v3) & A_n_vec_set$(v5)))) % 224.46/33.27 % 224.46/33.27 (axiom600) % 224.60/33.27 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.60/33.28 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.60/33.28 % 224.60/33.28 (axiom601) % 224.60/33.28 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.60/33.28 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.60/33.28 % 224.60/33.28 (axiom602) % 224.60/33.28 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.60/33.28 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.60/33.28 % 224.60/33.28 (axiom629) % 224.60/33.28 Nat_int_fun$(of_nat$) & ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | % 224.60/33.28 ~ (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.60/33.28 % 224.60/33.28 (axiom73) % 224.60/33.28 Nat$(zero$c) & Nat_nat_bool_fun_fun$(less$) & ? [v0: Nat_bool_fun$] : % 224.60/33.28 (fun_app$q(less$, zero$c) = v0 & Nat_bool_fun$(v0) & ~ (fun_app$g(v0, zero$c) % 224.60/33.28 = 0) & ! [v1: Nat$] : ! [v2: int] : (v2 = 0 | v1 = zero$c | ~ % 224.60/33.28 (fun_app$g(v0, v1) = v2) | ~ Nat$(v1))) % 224.60/33.28 % 224.60/33.28 (axiom76) % 224.60/33.28 Nat$(zero$c) & Nat_nat_bool_fun_fun$(less$) & ? [v0: Nat_bool_fun$] : % 224.60/33.28 (fun_app$q(less$, zero$c) = v0 & Nat_bool_fun$(v0) & ! [v1: Nat$] : ! [v2: % 224.60/33.28 int] : (v2 = 0 | v1 = zero$c | ~ (fun_app$g(v0, v1) = v2) | ~ Nat$(v1))) % 224.60/33.28 % 224.60/33.28 (axiom94) % 224.60/33.28 Nat_int_fun$(of_nat$) & A_rows_vec$(zero$) & % 224.60/33.28 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & ? [v0: % 224.60/33.28 A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.60/33.28 A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: A_rows_vec$] % 224.60/33.28 : ! [v3: A_rows_vec_bool_fun$] : ( ~ (consistent$a(v1) = v3) | ~ % 224.60/33.28 (fun_app$b(v3, v2) = 0) | ~ A_n_vec_rows_vec$(v1) | ~ A_rows_vec$(v2) | % 224.60/33.28 ? [v4: A_n_vec_set$] : ? [v5: Nat$] : ? [v6: int] : ( ~ (v6 = 0) & % 224.60/33.28 fun_app$k(v0, v4) = v5 & fun_app$j(of_nat$, v5) = v6 & solution_set$(v1, % 224.60/33.28 zero$) = v4 & Nat$(v5) & A_n_vec_set$(v4)) | ? [v4: A_n_vec$] : ? % 224.60/33.28 [v5: A_rows_vec_bool_fun$] : (is_solution$a(v4, v1) = v5 & fun_app$b(v5, % 224.60/33.28 v2) = 0 & A_n_vec$(v4) & A_rows_vec_bool_fun$(v5) & ! [v6: A_n_vec$] % 224.60/33.28 : ! [v7: A_rows_vec_bool_fun$] : (v6 = v4 | ~ (is_solution$a(v6, v1) = % 224.60/33.28 v7) | ~ (fun_app$b(v7, v2) = 0) | ~ A_n_vec$(v6))))) % 224.60/33.28 % 224.60/33.28 (axiom95) % 224.60/33.28 Nat$(zero$c) & Nat_nat_bool_fun_fun$(less$) & ? [v0: Nat_bool_fun$] : ? [v1: % 224.60/33.28 int] : ( ~ (v1 = 0) & fun_app$q(less$, zero$c) = v0 & fun_app$g(v0, zero$c) % 224.60/33.28 = v1 & Nat_bool_fun$(v0)) % 224.60/33.28 % 224.60/33.28 (axiom98) % 224.60/33.28 Nat_int_fun$(of_nat$) & Nat$(zero$c) & Nat_nat_fun$(of_nat$a) & % 224.60/33.28 Nat_nat_bool_fun_fun$(less$) & ? [v0: Nat_bool_fun$] : (fun_app$q(less$, % 224.60/33.28 zero$c) = v0 & Nat_bool_fun$(v0) & ! [v1: Nat$] : ! [v2: Nat$] : ( ~ % 224.60/33.28 (fun_app$r(of_nat$a, v1) = v2) | ~ Nat$(v1) | ? [v3: any] : ? [v4: int] % 224.60/33.29 : (fun_app$j(of_nat$, v1) = v4 & fun_app$g(v0, v2) = v3 & ( ~ (v3 = 0) | % 224.60/33.29 ~ ($lesseq(v4, 0)))) & ! [v1: Nat$] : ! [v2: Nat$] : ( ~ % 224.60/33.29 (fun_app$r(of_nat$a, v1) = v2) | ~ Nat$(v1) | ? [v3: int] : ? [v4: % 224.60/33.29 any] : (fun_app$j(of_nat$, v1) = v3 & fun_app$g(v0, v2) = v4 & (v4 = 0 % 224.60/33.29 | ~ ($lesseq(1, v3)))))) % 224.60/33.29 % 224.60/33.29 (conjecture6) % 224.60/33.29 Nat_int_fun$(of_nat$) & A_n_vec_rows_vec$(a$) & A_rows_vec$(zero$) & % 224.60/33.29 A_n_vec_set_bool_fun$(finite$) & % 224.60/33.29 A_a_n_vec_a_n_vec_fun_fun$(vector_scalar_mult$) & ? [v0: A_n_vec_set$] : ? % 224.60/33.29 [v1: any] : ? [v2: A_n_vec_set_nat_fun$] : ? [v3: Nat$] : ? [v4: int] : % 224.60/33.29 (dim$(vector_scalar_mult$) = v2 & fun_app$k(v2, v0) = v3 & fun_app$j(of_nat$, % 224.60/33.29 v3) = v4 & solution_set$(a$, zero$) = v0 & fun_app$d(finite$, v0) = v1 & % 224.60/33.29 A_n_vec_set_nat_fun$(v2) & Nat$(v3) & A_n_vec_set$(v0) & ((v1 = 0 & % 224.60/33.29 $lesseq(1, v4)) | ( ~ (v1 = 0) & $lesseq(v4, 0)))) % 224.60/33.29 % 224.60/33.29 (function-axioms) % 224.87/33.34 ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | % 224.87/33.34 ~ (real_$quotient(v3, v2) = v1) | ~ (real_$quotient(v3, v2) = v0)) & ! % 224.87/33.34 [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 224.87/33.34 (real_$difference(v3, v2) = v1) | ~ (real_$difference(v3, v2) = v0)) & ! % 224.87/33.34 [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 224.87/33.34 (real_$sum(v3, v2) = v1) | ~ (real_$sum(v3, v2) = v0)) & ! [v0: % 224.87/33.34 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 224.87/33.34 $real] : (v1 = v0 | ~ (real_$greatereq(v3, v2) = v1) | ~ % 224.87/33.34 (real_$greatereq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.34 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 224.87/33.34 (real_$greater(v3, v2) = v1) | ~ (real_$greater(v3, v2) = v0)) & ! [v0: % 224.87/33.34 Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_set$] : ! [v3: Nat_set$] : (v1 % 224.87/33.34 = v0 | ~ (times$f(v3, v2) = v1) | ~ (times$f(v3, v2) = v0)) & ! [v0: % 224.87/33.34 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_set$] : ! [v3: % 224.87/33.34 A_n_vec_set$] : (v1 = v0 | ~ (times$e(v3, v2) = v1) | ~ (times$e(v3, v2) = % 224.87/33.34 v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A$] : ! [v3: A$] : (v1 = v0 | % 224.87/33.34 ~ (times$d(v3, v2) = v1) | ~ (times$d(v3, v2) = v0)) & ! [v0: % 224.87/33.34 Real_real_fun$] : ! [v1: Real_real_fun$] : ! [v2: $real] : ! [v3: % 224.87/33.34 Real_real_real_fun_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ % 224.87/33.34 (fun_app$ad(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 224.87/33.34 $real] : ! [v3: $real] : (v1 = v0 | ~ (real_$product(v3, v2) = v1) | ~ % 224.87/33.34 (real_$product(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] % 224.87/33.34 : ! [v2: A_rows_vec$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ (times$c(v3, v2) % 224.87/33.34 = v1) | ~ (times$c(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 224.87/33.34 [v2: Real_set$] : ! [v3: Real_set_nat_fun$] : (v1 = v0 | ~ (fun_app$ac(v3, % 224.87/33.34 v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: % 224.87/33.34 Nat$] : ! [v2: Nat_set$] : ! [v3: Nat_real_fun$] : (v1 = v0 | ~ % 224.87/33.34 (arg_min_on$c(v3, v2) = v1) | ~ (arg_min_on$c(v3, v2) = v0)) & ! [v0: % 224.87/33.34 A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_set$] : ! [v3: % 224.87/33.34 A_n_vec_real_fun$] : (v1 = v0 | ~ (arg_min_on$b(v3, v2) = v1) | ~ % 224.87/33.34 (arg_min_on$b(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 224.87/33.34 A_n_vec$] : ! [v3: A_n_vec_real_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = % 224.87/33.34 v1) | ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 224.87/33.34 [v2: $real] : ! [v3: Real_real_fun$] : (v1 = v0 | ~ (fun_app$aa(v3, v2) = % 224.87/33.34 v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 224.87/33.34 [v2: int] : ! [v3: Int_real_fun$] : (v1 = v0 | ~ (fun_app$z(v3, v2) = v1) | % 224.87/33.34 ~ (fun_app$z(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: $real] : % 224.87/33.34 ! [v3: Real_int_fun$] : (v1 = v0 | ~ (fun_app$y(v3, v2) = v1) | ~ % 224.87/33.34 (fun_app$y(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.34 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 224.87/33.34 (real_$lesseq(v3, v2) = v1) | ~ (real_$lesseq(v3, v2) = v0)) & ! [v0: % 224.87/33.34 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_rows_vec_set$] : % 224.87/33.34 ! [v3: A_rows_vec_set$] : (v1 = v0 | ~ (less_eq$(v3, v2) = v1) | ~ % 224.87/33.34 (less_eq$(v3, v2) = v0)) & ! [v0: Real_set$] : ! [v1: Real_set$] : ! [v2: % 224.87/33.34 Real_set$] : ! [v3: $real] : (v1 = v0 | ~ (insert$d(v3, v2) = v1) | ~ % 224.87/33.34 (insert$d(v3, v2) = v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: % 224.87/33.34 Int_set$] : ! [v3: int] : (v1 = v0 | ~ (insert$c(v3, v2) = v1) | ~ % 224.87/33.34 (insert$c(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 224.87/33.34 Nat_set$] : ! [v3: Nat$] : (v1 = v0 | ~ (insert$b(v3, v2) = v1) | ~ % 224.87/33.34 (insert$b(v3, v2) = v0)) & ! [v0: A_n_vec_set$] : ! [v1: A_n_vec_set$] : % 224.87/33.34 ! [v2: A_n_vec_set$] : ! [v3: A_n_vec$] : (v1 = v0 | ~ (insert$a(v3, v2) = % 224.87/33.34 v1) | ~ (insert$a(v3, v2) = v0)) & ! [v0: A_rows_vec_set$] : ! [v1: % 224.87/33.34 A_rows_vec_set$] : ! [v2: A_rows_vec_set$] : ! [v3: A_rows_vec$] : (v1 = % 224.87/33.34 v0 | ~ (insert$(v3, v2) = v1) | ~ (insert$(v3, v2) = v0)) & ! [v0: Nat$] % 224.87/33.34 : ! [v1: Nat$] : ! [v2: Nat_set$] : ! [v3: Nat_int_fun$] : (v1 = v0 | ~ % 224.87/33.34 (arg_min_on$a(v3, v2) = v1) | ~ (arg_min_on$a(v3, v2) = v0)) & ! [v0: % 224.87/33.34 A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_set$] : ! [v3: % 224.87/33.34 A_n_vec_int_fun$] : (v1 = v0 | ~ (arg_min_on$(v3, v2) = v1) | ~ % 224.87/33.34 (arg_min_on$(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 224.87/33.34 A_n_vec$] : ! [v3: A_n_vec_int_fun$] : (v1 = v0 | ~ (fun_app$x(v3, v2) = % 224.87/33.34 v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 224.87/33.34 int] : ! [v3: Int_int_fun$] : (v1 = v0 | ~ (fun_app$w(v3, v2) = v1) | ~ % 224.87/33.34 (fun_app$w(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.34 MultipleValueBool] : ! [v2: A_n_vec_set_set$] : ! [v3: A_n_vec_set$] : (v1 % 224.87/33.34 = v0 | ~ (member$f(v3, v2) = v1) | ~ (member$f(v3, v2) = v0)) & ! [v0: % 224.87/33.34 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set_set$] : ! % 224.87/33.34 [v3: Nat_set$] : (v1 = v0 | ~ (member$e(v3, v2) = v1) | ~ (member$e(v3, v2) % 224.87/33.34 = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 224.87/33.34 A_n_vec$] : ! [v3: A_n_vec_a_n_vec_bool_fun_fun$] : (v1 = v0 | ~ % 224.87/33.34 (fun_app$v(v3, v2) = v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: % 224.87/33.34 Real_bool_fun$] : ! [v1: Real_bool_fun$] : ! [v2: $real] : ! [v3: % 224.87/33.34 Real_real_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$u(v3, v2) = v1) | ~ % 224.87/33.34 (fun_app$u(v3, v2) = v0)) & ! [v0: A_rows_vec_bool_fun$] : ! [v1: % 224.87/33.34 A_rows_vec_bool_fun$] : ! [v2: A_rows_vec$] : ! [v3: % 224.87/33.34 A_rows_vec_a_rows_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) = % 224.87/33.34 v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: % 224.87/33.34 A_rows_vec$] : ! [v2: A$] : ! [v3: Rows$] : (v1 = v0 | ~ (axis$(v3, v2) = % 224.87/33.34 v1) | ~ (axis$(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 224.87/33.35 Nat$] : ! [v3: Nat_real_fun$] : (v1 = v0 | ~ (fun_app$s(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$s(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat$] : % 224.87/33.35 ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$r(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.35 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 224.87/33.35 (real_$less(v3, v2) = v1) | ~ (real_$less(v3, v2) = v0)) & ! [v0: % 224.87/33.35 A_rows_vec_bool_fun$] : ! [v1: A_rows_vec_bool_fun$] : ! [v2: % 224.87/33.35 A_n_vec_rows_vec$] : ! [v3: A_n_vec$] : (v1 = v0 | ~ (is_solution$a(v3, % 224.87/33.35 v2) = v1) | ~ (is_solution$a(v3, v2) = v0)) & ! [v0: % 224.87/33.35 A_rows_vec_bool_fun$] : ! [v1: A_rows_vec_bool_fun$] : ! [v2: % 224.87/33.35 A_rows_vec_rows_vec$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ % 224.87/33.35 (is_solution$(v3, v2) = v1) | ~ (is_solution$(v3, v2) = v0)) & ! [v0: % 224.87/33.35 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : ! [v3: % 224.87/33.35 Nat_nat_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$q(v3, v2) = v0)) & ! [v0: A_n_vec_a_n_vec_fun$] : ! [v1: % 224.87/33.35 A_n_vec_a_n_vec_fun$] : ! [v2: A$] : ! [v3: A_a_n_vec_a_n_vec_fun_fun$] : % 224.87/33.35 (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) & ! % 224.87/33.35 [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec$] : ! [v3: % 224.87/33.35 A_n_vec_a_n_vec_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$o(v3, v2) = v0)) & ! [v0: A_rows_vec_a_rows_vec_fun$] : ! [v1: % 224.87/33.35 A_rows_vec_a_rows_vec_fun$] : ! [v2: A$] : ! [v3: % 224.87/33.35 A_a_rows_vec_a_rows_vec_fun_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | % 224.87/33.35 ~ (fun_app$n(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : % 224.87/33.35 ! [v2: A_rows_vec$] : ! [v3: A_rows_vec_a_rows_vec_fun$] : (v1 = v0 | ~ % 224.87/33.35 (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: Nat$] : ! % 224.87/33.35 [v1: Nat$] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_set_nat_fun$] : (v1 = v0 % 224.87/33.35 | ~ (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: Nat$] % 224.87/33.35 : ! [v1: Nat$] : ! [v2: A_rows_vec_set$] : ! [v3: A_rows_vec_set_nat_fun$] % 224.87/33.35 : (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! % 224.87/33.35 [v0: int] : ! [v1: int] : ! [v2: Nat$] : ! [v3: Nat_int_fun$] : (v1 = v0 | % 224.87/33.35 ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! [v0: % 224.87/33.35 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_rows_vec$] : ! [v3: % 224.87/33.35 A_n_vec_rows_vec$] : (v1 = v0 | ~ (solution_set$(v3, v2) = v1) | ~ % 224.87/33.35 (solution_set$(v3, v2) = v0)) & ! [v0: A_rows_vec_set$] : ! [v1: % 224.87/33.35 A_rows_vec_set$] : ! [v2: A_rows_vec$] : ! [v3: A_rows_vec_rows_vec$] : % 224.87/33.35 (v1 = v0 | ~ (solution_set$a(v3, v2) = v1) | ~ (solution_set$a(v3, v2) = % 224.87/33.35 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 224.87/33.35 Int_set$] : ! [v3: Int_set_bool_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = % 224.87/33.35 v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.35 MultipleValueBool] : ! [v2: Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ % 224.87/33.35 (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! % 224.87/33.35 [v3: Nat_set_bool_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$h(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.35 MultipleValueBool] : ! [v2: $real] : ! [v3: Real_bool_fun$] : (v1 = v0 | % 224.87/33.35 ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Real_set$] : ! % 224.87/33.35 [v3: Real_set_bool_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$f(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.35 MultipleValueBool] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_bool_fun$] : (v1 = % 224.87/33.35 v0 | ~ (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_n_vec_set$] : ! % 224.87/33.35 [v3: A_n_vec_set_bool_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 224.87/33.35 (fun_app$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 224.87/33.35 MultipleValueBool] : ! [v2: A_rows_vec$] : ! [v3: A_rows_vec_bool_fun$] : % 224.87/33.35 (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = v0)) & ! % 224.87/33.35 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 224.87/33.35 A_rows_vec_set$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ (member$(v3, v2) = % 224.87/33.35 v1) | ~ (member$(v3, v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: % 224.87/33.35 Int_bool_fun$] : ! [v2: int] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | % 224.87/33.35 ~ (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 224.87/33.35 Int_bool_fun$] : (v1 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, % 224.87/33.35 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 224.87/33.35 ! [v2: $real] : (v1 = v0 | ~ (real_$is_int(v2) = v1) | ~ (real_$is_int(v2) = % 224.87/33.35 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 224.87/33.35 $real] : (v1 = v0 | ~ (real_$is_rat(v2) = v1) | ~ (real_$is_rat(v2) = v0)) % 224.87/33.35 & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 224.87/33.35 (real_$floor(v2) = v1) | ~ (real_$floor(v2) = v0)) & ! [v0: $real] : ! % 224.87/33.35 [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$ceiling(v2) = v1) | ~ % 224.87/33.35 (real_$ceiling(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] % 224.87/33.35 : (v1 = v0 | ~ (real_$truncate(v2) = v1) | ~ (real_$truncate(v2) = v0)) & ! % 224.87/33.35 [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$round(v2) % 224.87/33.35 = v1) | ~ (real_$round(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 224.87/33.35 $real] : (v1 = v0 | ~ (real_$to_int(v2) = v1) | ~ (real_$to_int(v2) = v0)) % 224.87/33.35 & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $real] : (v1 = v0 | ~ % 224.87/33.35 (real_$to_rat(v2) = v1) | ~ (real_$to_rat(v2) = v0)) & ! [v0: $real] : ! % 224.87/33.35 [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_real(v2) = v1) | ~ % 224.87/33.35 (real_$to_real(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: int] : % 224.87/33.35 (v1 = v0 | ~ (int_$to_real(v2) = v1) | ~ (int_$to_real(v2) = v0)) & ! [v0: % 224.87/33.35 $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$uminus(v2) = % 224.87/33.35 v1) | ~ (real_$uminus(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 224.87/33.35 [v2: Real_set$] : (v1 = v0 | ~ (card$b(v2) = v1) | ~ (card$b(v2) = v0)) & ! % 224.87/33.35 [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_set$] : (v1 = v0 | ~ (card$a(v2) = % 224.87/33.35 v1) | ~ (card$a(v2) = v0)) & ! [v0: Nat_nat_fun$] : ! [v1: % 224.87/33.35 Nat_nat_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ (times$b(v2) = v1) | ~ % 224.87/33.35 (times$b(v2) = v0)) & ! [v0: Int_int_fun$] : ! [v1: Int_int_fun$] : ! % 224.87/33.35 [v2: int] : (v1 = v0 | ~ (times$a(v2) = v1) | ~ (times$a(v2) = v0)) & ! % 224.87/33.35 [v0: Real_set_bool_fun$] : ! [v1: Real_set_bool_fun$] : ! [v2: Real_set$] : % 224.87/33.35 (v1 = v0 | ~ (less_eq$d(v2) = v1) | ~ (less_eq$d(v2) = v0)) & ! [v0: Nat$] % 224.87/33.35 : ! [v1: Nat$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (card$(v2) = v1) | ~ % 224.87/33.35 (card$(v2) = v0)) & ! [v0: Nat_set_bool_fun$] : ! [v1: Nat_set_bool_fun$] % 224.87/33.35 : ! [v2: Nat_set$] : (v1 = v0 | ~ (less_eq$b(v2) = v1) | ~ (less_eq$b(v2) = % 224.87/33.35 v0)) & ! [v0: A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : % 224.87/33.35 ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (less_eq$a(v2) = v1) | ~ (less_eq$a(v2) % 224.87/33.35 = v0)) & ! [v0: Nat_nat_fun$] : ! [v1: Nat_nat_fun$] : ! [v2: Nat_set$] % 224.87/33.35 : (v1 = v0 | ~ (enumerate$(v2) = v1) | ~ (enumerate$(v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_n_vec_set_set$] % 224.87/33.35 : (v1 = v0 | ~ (finite$f(v2) = v1) | ~ (finite$f(v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set_set$] : % 224.87/33.35 (v1 = v0 | ~ (finite$e(v2) = v1) | ~ (finite$e(v2) = v0)) & ! [v0: A$] : ! % 224.87/33.35 [v1: A$] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$d(v2) = v1) | ~ % 224.87/33.35 (of_nat$d(v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! [v2: % 224.87/33.35 Nat$] : (v1 = v0 | ~ (of_nat$c(v2) = v1) | ~ (of_nat$c(v2) = v0)) & ! % 224.87/33.35 [v0: A_rows_vec_bool_fun$] : ! [v1: A_rows_vec_bool_fun$] : ! [v2: % 224.87/33.35 A_n_vec_rows_vec$] : (v1 = v0 | ~ (inconsistent$(v2) = v1) | ~ % 224.87/33.35 (inconsistent$(v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! % 224.87/33.35 [v2: A$] : (v1 = v0 | ~ (vec$(v2) = v1) | ~ (vec$(v2) = v0)) & ! [v0: % 224.87/33.35 Real_set_nat_fun$] : ! [v1: Real_set_nat_fun$] : ! [v2: % 224.87/33.35 Real_real_real_fun_fun$] : (v1 = v0 | ~ (dim$b(v2) = v1) | ~ (dim$b(v2) = % 224.87/33.35 v0)) & ! [v0: A_rows_vec_bool_fun$] : ! [v1: A_rows_vec_bool_fun$] : ! % 224.87/33.35 [v2: A_n_vec_rows_vec$] : (v1 = v0 | ~ (consistent$a(v2) = v1) | ~ % 224.87/33.35 (consistent$a(v2) = v0)) & ! [v0: A_rows_vec_bool_fun$] : ! [v1: % 224.87/33.35 A_rows_vec_bool_fun$] : ! [v2: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 224.87/33.35 (consistent$(v2) = v1) | ~ (consistent$(v2) = v0)) & ! [v0: % 224.87/33.35 Nat_set_bool_fun$] : ! [v1: Nat_set_bool_fun$] : ! [v2: Nat_set$] : (v1 = % 224.87/33.35 v0 | ~ (less$d(v2) = v1) | ~ (less$d(v2) = v0)) & ! [v0: % 224.87/33.35 A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : ! [v2: % 224.87/33.35 A_n_vec_set$] : (v1 = v0 | ~ (less$c(v2) = v1) | ~ (less$c(v2) = v0)) & ! % 224.87/33.35 [v0: Real_set_bool_fun$] : ! [v1: Real_set_bool_fun$] : ! [v2: Real_set$] : % 224.87/33.35 (v1 = v0 | ~ (less$b(v2) = v1) | ~ (less$b(v2) = v0)) & ! [v0: % 224.87/33.35 Int_set_bool_fun$] : ! [v1: Int_set_bool_fun$] : ! [v2: Int_set$] : (v1 = % 224.87/33.35 v0 | ~ (less$a(v2) = v1) | ~ (less$a(v2) = v0)) & ! [v0: Nat_set$] : ! % 224.87/33.35 [v1: Nat_set$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (collect$d(v2) = v1) | % 224.87/33.35 ~ (collect$d(v2) = v0)) & ! [v0: Real_set$] : ! [v1: Real_set$] : ! [v2: % 224.87/33.35 Real_bool_fun$] : (v1 = v0 | ~ (collect$c(v2) = v1) | ~ (collect$c(v2) = % 224.87/33.35 v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: Int_bool_fun$] : % 224.87/33.35 (v1 = v0 | ~ (collect$b(v2) = v1) | ~ (collect$b(v2) = v0)) & ! [v0: % 224.87/33.35 A_rows_vec_set$] : ! [v1: A_rows_vec_set$] : ! [v2: A_rows_vec_bool_fun$] % 224.87/33.35 : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ (collect$a(v2) = v0)) & ! [v0: % 224.87/33.35 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_bool_fun$] : (v1 = % 224.87/33.35 v0 | ~ (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & ! [v0: % 224.87/33.35 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_rows_vec$] : (v1 = % 224.87/33.35 v0 | ~ (null_space$a(v2) = v1) | ~ (null_space$a(v2) = v0)) & ! [v0: % 224.87/33.35 A_rows_vec_set$] : ! [v1: A_rows_vec_set$] : ! [v2: A_rows_vec_rows_vec$] % 224.87/33.35 : (v1 = v0 | ~ (null_space$(v2) = v1) | ~ (null_space$(v2) = v0)) & ! [v0: % 224.87/33.35 Nat$] : ! [v1: Nat$] : ! [v2: int] : (v1 = v0 | ~ (nat$(v2) = v1) | ~ % 224.87/33.35 (nat$(v2) = v0)) & ! [v0: A_n_vec_set_nat_fun$] : ! [v1: % 224.87/33.35 A_n_vec_set_nat_fun$] : ! [v2: A_a_n_vec_a_n_vec_fun_fun$] : (v1 = v0 | ~ % 224.87/33.35 (dim$(v2) = v1) | ~ (dim$(v2) = v0)) & ! [v0: A_rows_vec_set_nat_fun$] : % 224.87/33.35 ! [v1: A_rows_vec_set_nat_fun$] : ! [v2: A_a_rows_vec_a_rows_vec_fun_fun$] : % 224.87/33.35 (v1 = v0 | ~ (dim$a(v2) = v1) | ~ (dim$a(v2) = v0)) & ! [v0: % 224.87/33.35 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_rows_vec_set$] : % 224.87/33.35 (v1 = v0 | ~ (finite$a(v2) = v1) | ~ (finite$a(v2) = v0)) & ! [v0: % 224.87/33.35 Int_bool_fun$] : ! [v1: Int_bool_fun$] : ! [v2: Int_set$] : (v1 = v0 | ~ % 224.87/33.35 (uub$(v2) = v1) | ~ (uub$(v2) = v0)) & ! [v0: Int_set_bool_fun$] : ! [v1: % 224.87/33.35 Int_set_bool_fun$] : ! [v2: int] : (v1 = v0 | ~ (member$d(v2) = v1) | ~ % 224.87/33.35 (member$d(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! % 224.87/33.35 [v2: Nat_set$] : (v1 = v0 | ~ (uud$(v2) = v1) | ~ (uud$(v2) = v0)) & ! [v0: % 224.87/33.35 Nat_set_bool_fun$] : ! [v1: Nat_set_bool_fun$] : ! [v2: Nat$] : (v1 = v0 | % 224.87/33.35 ~ (member$c(v2) = v1) | ~ (member$c(v2) = v0)) & ! [v0: Real_bool_fun$] : % 224.87/33.35 ! [v1: Real_bool_fun$] : ! [v2: Real_set$] : (v1 = v0 | ~ (uuc$(v2) = v1) | % 224.87/33.35 ~ (uuc$(v2) = v0)) & ! [v0: Real_set_bool_fun$] : ! [v1: % 224.87/33.35 Real_set_bool_fun$] : ! [v2: $real] : (v1 = v0 | ~ (member$b(v2) = v1) | % 224.87/33.35 ~ (member$b(v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 224.87/33.35 A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (uu$(v2) = v1) | % 224.87/33.35 ~ (uu$(v2) = v0)) & ! [v0: A_n_vec_set_bool_fun$] : ! [v1: % 224.87/33.35 A_n_vec_set_bool_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (member$a(v2) = % 224.87/33.35 v1) | ~ (member$a(v2) = v0)) & ! [v0: A_rows_vec_bool_fun$] : ! [v1: % 224.87/33.35 A_rows_vec_bool_fun$] : ! [v2: A_rows_vec_set$] : (v1 = v0 | ~ (uua$(v2) = % 224.87/33.35 v1) | ~ (uua$(v2) = v0)) & ? [v0: $real] : ? [v1: $real] : ? [v2: % 224.87/33.35 $real] : (real_$quotient(v1, v0) = v2) & ? [v0: $real] : ? [v1: $real] : % 224.87/33.35 ? [v2: $real] : (real_$difference(v1, v0) = v2) & ? [v0: $real] : ? [v1: % 224.87/33.35 $real] : ? [v2: $real] : (real_$sum(v1, v0) = v2) & ? [v0: $real] : ? % 224.87/33.35 [v1: $real] : ? [v2: MultipleValueBool] : (real_$greatereq(v1, v0) = v2) & ? % 224.87/33.35 [v0: $real] : ? [v1: $real] : ? [v2: MultipleValueBool] : (real_$greater(v1, % 224.87/33.35 v0) = v2) & ? [v0: $real] : ? [v1: $real] : ? [v2: $real] : % 224.87/33.35 (real_$product(v1, v0) = v2) & ? [v0: A_n_vec$] : ? [v1: A_n_vec_real_fun$] % 224.87/33.35 : ? [v2: $real] : (fun_app$ab(v1, v0) = v2) & ? [v0: $real] : ? [v1: % 224.87/33.35 Real_real_fun$] : ? [v2: $real] : (fun_app$aa(v1, v0) = v2) & ? [v0: int] % 224.87/33.35 : ? [v1: Int_real_fun$] : ? [v2: $real] : (fun_app$z(v1, v0) = v2) & ? [v0: % 224.87/33.35 $real] : ? [v1: Real_int_fun$] : ? [v2: int] : (fun_app$y(v1, v0) = v2) & % 224.87/33.35 ? [v0: $real] : ? [v1: $real] : ? [v2: MultipleValueBool] : % 224.87/33.35 (real_$lesseq(v1, v0) = v2) & ? [v0: A_rows_vec_set$] : ? [v1: % 224.87/33.35 A_rows_vec_set$] : ? [v2: MultipleValueBool] : (less_eq$(v1, v0) = v2) & ? % 224.87/33.35 [v0: A_n_vec$] : ? [v1: A_n_vec_int_fun$] : ? [v2: int] : (fun_app$x(v1, v0) % 224.87/33.35 = v2) & ? [v0: int] : ? [v1: Int_int_fun$] : ? [v2: int] : (fun_app$w(v1, % 224.87/33.35 v0) = v2) & ? [v0: A_n_vec_set_set$] : ? [v1: A_n_vec_set$] : ? [v2: % 224.87/33.35 MultipleValueBool] : (member$f(v1, v0) = v2) & ? [v0: Nat_set_set$] : ? % 224.87/33.35 [v1: Nat_set$] : ? [v2: MultipleValueBool] : (member$e(v1, v0) = v2) & ? % 224.87/33.35 [v0: Nat$] : ? [v1: Nat_real_fun$] : ? [v2: $real] : (fun_app$s(v1, v0) = % 224.87/33.35 v2) & ? [v0: $real] : ? [v1: $real] : ? [v2: MultipleValueBool] : % 224.87/33.35 (real_$less(v1, v0) = v2) & ? [v0: Nat$] : ? [v1: Nat_int_fun$] : ? [v2: % 224.87/33.35 int] : (fun_app$j(v1, v0) = v2) & ? [v0: Int_set$] : ? [v1: % 224.87/33.35 Int_set_bool_fun$] : ? [v2: MultipleValueBool] : (fun_app$i(v1, v0) = v2) & % 224.87/33.35 ? [v0: Nat$] : ? [v1: Nat_bool_fun$] : ? [v2: MultipleValueBool] : % 224.87/33.35 (fun_app$g(v1, v0) = v2) & ? [v0: Nat_set$] : ? [v1: Nat_set_bool_fun$] : ? % 224.87/33.35 [v2: MultipleValueBool] : (fun_app$h(v1, v0) = v2) & ? [v0: $real] : ? [v1: % 224.87/33.35 Real_bool_fun$] : ? [v2: MultipleValueBool] : (fun_app$e(v1, v0) = v2) & ? % 224.87/33.35 [v0: Real_set$] : ? [v1: Real_set_bool_fun$] : ? [v2: MultipleValueBool] : % 224.87/33.35 (fun_app$f(v1, v0) = v2) & ? [v0: A_n_vec$] : ? [v1: A_n_vec_bool_fun$] : ? % 224.87/33.35 [v2: MultipleValueBool] : (fun_app$c(v1, v0) = v2) & ? [v0: A_n_vec_set$] : % 224.97/33.35 ? [v1: A_n_vec_set_bool_fun$] : ? [v2: MultipleValueBool] : (fun_app$d(v1, % 224.97/33.35 v0) = v2) & ? [v0: A_rows_vec$] : ? [v1: A_rows_vec_bool_fun$] : ? [v2: % 224.97/33.35 MultipleValueBool] : (fun_app$b(v1, v0) = v2) & ? [v0: A_rows_vec_set$] : % 224.97/33.35 ? [v1: A_rows_vec$] : ? [v2: MultipleValueBool] : (member$(v1, v0) = v2) & ? % 224.97/33.35 [v0: int] : ? [v1: Int_bool_fun$] : ? [v2: MultipleValueBool] : % 224.97/33.35 (fun_app$(v1, v0) = v2) & ? [v0: Nat_set$] : ? [v1: Nat_set$] : ? [v2: % 224.97/33.35 Nat_set$] : (times$f(v1, v0) = v2 & Nat_set$(v2)) & ? [v0: A_n_vec_set$] : % 224.97/33.35 ? [v1: A_n_vec_set$] : ? [v2: A_n_vec_set$] : (times$e(v1, v0) = v2 & % 224.97/33.35 A_n_vec_set$(v2)) & ? [v0: A$] : ? [v1: A$] : ? [v2: A$] : (times$d(v1, % 224.97/33.35 v0) = v2 & A$(v2)) & ? [v0: $real] : ? [v1: Real_real_real_fun_fun$] : % 224.97/33.35 ? [v2: Real_real_fun$] : (fun_app$ad(v1, v0) = v2 & Real_real_fun$(v2)) & ? % 224.97/33.35 [v0: A_rows_vec$] : ? [v1: A_rows_vec$] : ? [v2: A_rows_vec$] : (times$c(v1, % 224.97/33.35 v0) = v2 & A_rows_vec$(v2)) & ? [v0: Real_set$] : ? [v1: % 224.97/33.35 Real_set_nat_fun$] : ? [v2: Nat$] : (fun_app$ac(v1, v0) = v2 & Nat$(v2)) & % 224.97/33.35 ? [v0: Nat_set$] : ? [v1: Nat_real_fun$] : ? [v2: Nat$] : (arg_min_on$c(v1, % 224.97/33.35 v0) = v2 & Nat$(v2)) & ? [v0: A_n_vec_set$] : ? [v1: A_n_vec_real_fun$] % 224.97/33.35 : ? [v2: A_n_vec$] : (arg_min_on$b(v1, v0) = v2 & A_n_vec$(v2)) & ? [v0: % 224.97/33.35 Real_set$] : ? [v1: $real] : ? [v2: Real_set$] : (insert$d(v1, v0) = v2 & % 224.97/33.35 Real_set$(v2)) & ? [v0: Int_set$] : ? [v1: int] : ? [v2: Int_set$] : % 224.97/33.35 (insert$c(v1, v0) = v2 & Int_set$(v2)) & ? [v0: Nat_set$] : ? [v1: Nat$] : % 224.97/33.35 ? [v2: Nat_set$] : (insert$b(v1, v0) = v2 & Nat_set$(v2)) & ? [v0: % 224.97/33.35 A_n_vec_set$] : ? [v1: A_n_vec$] : ? [v2: A_n_vec_set$] : (insert$a(v1, % 224.97/33.35 v0) = v2 & A_n_vec_set$(v2)) & ? [v0: A_rows_vec_set$] : ? [v1: % 224.97/33.35 A_rows_vec$] : ? [v2: A_rows_vec_set$] : (insert$(v1, v0) = v2 & % 224.97/33.35 A_rows_vec_set$(v2)) & ? [v0: Nat_set$] : ? [v1: Nat_int_fun$] : ? [v2: % 224.97/33.35 Nat$] : (arg_min_on$a(v1, v0) = v2 & Nat$(v2)) & ? [v0: A_n_vec_set$] : ? % 224.97/33.35 [v1: A_n_vec_int_fun$] : ? [v2: A_n_vec$] : (arg_min_on$(v1, v0) = v2 & % 224.97/33.35 A_n_vec$(v2)) & ? [v0: A_n_vec$] : ? [v1: A_n_vec_a_n_vec_bool_fun_fun$] : % 224.97/33.35 ? [v2: A_n_vec_bool_fun$] : (fun_app$v(v1, v0) = v2 & A_n_vec_bool_fun$(v2)) % 224.97/33.35 & ? [v0: $real] : ? [v1: Real_real_bool_fun_fun$] : ? [v2: Real_bool_fun$] % 224.97/33.35 : (fun_app$u(v1, v0) = v2 & Real_bool_fun$(v2)) & ? [v0: A_rows_vec$] : ? % 224.97/33.35 [v1: A_rows_vec_a_rows_vec_bool_fun_fun$] : ? [v2: A_rows_vec_bool_fun$] : % 224.97/33.35 (fun_app$t(v1, v0) = v2 & A_rows_vec_bool_fun$(v2)) & ? [v0: A$] : ? [v1: % 224.97/33.35 Rows$] : ? [v2: A_rows_vec$] : (axis$(v1, v0) = v2 & A_rows_vec$(v2)) & ? % 224.97/33.35 [v0: Nat$] : ? [v1: Nat_nat_fun$] : ? [v2: Nat$] : (fun_app$r(v1, v0) = v2 & % 224.97/33.35 Nat$(v2)) & ? [v0: A_n_vec_rows_vec$] : ? [v1: A_n_vec$] : ? [v2: % 224.97/33.35 A_rows_vec_bool_fun$] : (is_solution$a(v1, v0) = v2 & % 224.97/33.35 A_rows_vec_bool_fun$(v2)) & ? [v0: A_rows_vec_rows_vec$] : ? [v1: % 224.97/33.35 A_rows_vec$] : ? [v2: A_rows_vec_bool_fun$] : (is_solution$(v1, v0) = v2 & % 224.97/33.35 A_rows_vec_bool_fun$(v2)) & ? [v0: Nat$] : ? [v1: Nat_nat_bool_fun_fun$] : % 224.97/33.35 ? [v2: Nat_bool_fun$] : (fun_app$q(v1, v0) = v2 & Nat_bool_fun$(v2)) & ? % 224.97/33.35 [v0: A$] : ? [v1: A_a_n_vec_a_n_vec_fun_fun$] : ? [v2: A_n_vec_a_n_vec_fun$] % 224.97/33.35 : (fun_app$p(v1, v0) = v2 & A_n_vec_a_n_vec_fun$(v2)) & ? [v0: A_n_vec$] : ? % 224.97/33.35 [v1: A_n_vec_a_n_vec_fun$] : ? [v2: A_n_vec$] : (fun_app$o(v1, v0) = v2 & % 224.97/33.35 A_n_vec$(v2)) & ? [v0: A$] : ? [v1: A_a_rows_vec_a_rows_vec_fun_fun$] : ? % 224.97/33.35 [v2: A_rows_vec_a_rows_vec_fun$] : (fun_app$n(v1, v0) = v2 & % 224.97/33.35 A_rows_vec_a_rows_vec_fun$(v2)) & ? [v0: A_rows_vec$] : ? [v1: % 224.97/33.35 A_rows_vec_a_rows_vec_fun$] : ? [v2: A_rows_vec$] : (fun_app$m(v1, v0) = v2 % 224.97/33.35 & A_rows_vec$(v2)) & ? [v0: A_n_vec_set$] : ? [v1: A_n_vec_set_nat_fun$] : % 224.97/33.35 ? [v2: Nat$] : (fun_app$k(v1, v0) = v2 & Nat$(v2)) & ? [v0: A_rows_vec_set$] % 224.97/33.35 : ? [v1: A_rows_vec_set_nat_fun$] : ? [v2: Nat$] : (fun_app$l(v1, v0) = v2 & % 224.97/33.35 Nat$(v2)) & ? [v0: A_rows_vec$] : ? [v1: A_n_vec_rows_vec$] : ? [v2: % 224.97/33.35 A_n_vec_set$] : (solution_set$(v1, v0) = v2 & A_n_vec_set$(v2)) & ? [v0: % 224.97/33.35 A_rows_vec$] : ? [v1: A_rows_vec_rows_vec$] : ? [v2: A_rows_vec_set$] : % 224.97/33.35 (solution_set$a(v1, v0) = v2 & A_rows_vec_set$(v2)) & ? [v0: int] : ? [v1: % 224.97/33.35 Int_int_bool_fun_fun$] : ? [v2: Int_bool_fun$] : (fun_app$a(v1, v0) = v2 & % 224.97/33.35 Int_bool_fun$(v2)) & ? [v0: $real] : ? [v1: MultipleValueBool] : % 224.97/33.35 (real_$is_int(v0) = v1) & ? [v0: $real] : ? [v1: MultipleValueBool] : % 224.97/33.35 (real_$is_rat(v0) = v1) & ? [v0: $real] : ? [v1: $real] : (real_$floor(v0) = % 224.97/33.35 v1) & ? [v0: $real] : ? [v1: $real] : (real_$ceiling(v0) = v1) & ? [v0: % 224.97/33.35 $real] : ? [v1: $real] : (real_$truncate(v0) = v1) & ? [v0: $real] : ? % 224.97/33.35 [v1: $real] : (real_$round(v0) = v1) & ? [v0: $real] : ? [v1: int] : % 224.97/33.35 (real_$to_int(v0) = v1) & ? [v0: $real] : ? [v1: $rat] : (real_$to_rat(v0) = % 224.97/33.35 v1) & ? [v0: $real] : ? [v1: $real] : (real_$to_real(v0) = v1) & ? [v0: % 224.97/33.35 int] : ? [v1: $real] : (int_$to_real(v0) = v1) & ? [v0: $real] : ? [v1: % 224.97/33.35 $real] : (real_$uminus(v0) = v1) & ? [v0: A_n_vec_set_set$] : ? [v1: % 224.97/33.35 MultipleValueBool] : (finite$f(v0) = v1) & ? [v0: Nat_set_set$] : ? [v1: % 224.97/33.35 MultipleValueBool] : (finite$e(v0) = v1) & ? [v0: A_rows_vec_set$] : ? % 224.97/33.35 [v1: MultipleValueBool] : (finite$a(v0) = v1) & ? [v0: Real_set$] : ? [v1: % 224.97/33.35 Nat$] : (card$b(v0) = v1 & Nat$(v1)) & ? [v0: Nat_set$] : ? [v1: Nat$] : % 224.97/33.35 (card$a(v0) = v1 & Nat$(v1)) & ? [v0: Nat$] : ? [v1: Nat_nat_fun$] : % 224.97/33.35 (times$b(v0) = v1 & Nat_nat_fun$(v1)) & ? [v0: int] : ? [v1: Int_int_fun$] : % 224.97/33.35 (times$a(v0) = v1 & Int_int_fun$(v1)) & ? [v0: Real_set$] : ? [v1: % 224.97/33.35 Real_set_bool_fun$] : (less_eq$d(v0) = v1 & Real_set_bool_fun$(v1)) & ? % 224.97/33.35 [v0: A_n_vec_set$] : ? [v1: Nat$] : (card$(v0) = v1 & Nat$(v1)) & ? [v0: % 224.97/33.35 Nat_set$] : ? [v1: Nat_set_bool_fun$] : (less_eq$b(v0) = v1 & % 224.97/33.35 Nat_set_bool_fun$(v1)) & ? [v0: A_n_vec_set$] : ? [v1: % 224.97/33.35 A_n_vec_set_bool_fun$] : (less_eq$a(v0) = v1 & A_n_vec_set_bool_fun$(v1)) & % 224.97/33.35 ? [v0: Nat_set$] : ? [v1: Nat_nat_fun$] : (enumerate$(v0) = v1 & % 224.97/33.35 Nat_nat_fun$(v1)) & ? [v0: Nat$] : ? [v1: A$] : (of_nat$d(v0) = v1 & % 224.97/33.35 A$(v1)) & ? [v0: Nat$] : ? [v1: A_rows_vec$] : (of_nat$c(v0) = v1 & % 224.97/33.35 A_rows_vec$(v1)) & ? [v0: A_n_vec_rows_vec$] : ? [v1: % 224.97/33.35 A_rows_vec_bool_fun$] : (inconsistent$(v0) = v1 & A_rows_vec_bool_fun$(v1)) % 224.97/33.35 & ? [v0: A$] : ? [v1: A_rows_vec$] : (vec$(v0) = v1 & A_rows_vec$(v1)) & ? % 224.97/33.35 [v0: Real_real_real_fun_fun$] : ? [v1: Real_set_nat_fun$] : (dim$b(v0) = v1 & % 224.97/33.35 Real_set_nat_fun$(v1)) & ? [v0: A_n_vec_rows_vec$] : ? [v1: % 224.97/33.35 A_rows_vec_bool_fun$] : (consistent$a(v0) = v1 & A_rows_vec_bool_fun$(v1)) & % 224.97/33.35 ? [v0: A_rows_vec_rows_vec$] : ? [v1: A_rows_vec_bool_fun$] : % 224.97/33.35 (consistent$(v0) = v1 & A_rows_vec_bool_fun$(v1)) & ? [v0: Nat_set$] : ? % 224.97/33.35 [v1: Nat_set_bool_fun$] : (less$d(v0) = v1 & Nat_set_bool_fun$(v1)) & ? [v0: % 224.97/33.35 A_n_vec_set$] : ? [v1: A_n_vec_set_bool_fun$] : (less$c(v0) = v1 & % 224.97/33.35 A_n_vec_set_bool_fun$(v1)) & ? [v0: Real_set$] : ? [v1: % 224.97/33.35 Real_set_bool_fun$] : (less$b(v0) = v1 & Real_set_bool_fun$(v1)) & ? [v0: % 224.97/33.35 Int_set$] : ? [v1: Int_set_bool_fun$] : (less$a(v0) = v1 & % 224.97/33.35 Int_set_bool_fun$(v1)) & ? [v0: Nat_bool_fun$] : ? [v1: Nat_set$] : % 224.97/33.35 (collect$d(v0) = v1 & Nat_set$(v1)) & ? [v0: Real_bool_fun$] : ? [v1: % 224.97/33.35 Real_set$] : (collect$c(v0) = v1 & Real_set$(v1)) & ? [v0: Int_bool_fun$] : % 224.97/33.35 ? [v1: Int_set$] : (collect$b(v0) = v1 & Int_set$(v1)) & ? [v0: % 224.97/33.35 A_rows_vec_bool_fun$] : ? [v1: A_rows_vec_set$] : (collect$a(v0) = v1 & % 224.97/33.35 A_rows_vec_set$(v1)) & ? [v0: A_n_vec_bool_fun$] : ? [v1: A_n_vec_set$] : % 224.97/33.35 (collect$(v0) = v1 & A_n_vec_set$(v1)) & ? [v0: A_n_vec_rows_vec$] : ? [v1: % 224.97/33.35 A_n_vec_set$] : (null_space$a(v0) = v1 & A_n_vec_set$(v1)) & ? [v0: % 224.97/33.35 A_rows_vec_rows_vec$] : ? [v1: A_rows_vec_set$] : (null_space$(v0) = v1 & % 224.97/33.35 A_rows_vec_set$(v1)) & ? [v0: int] : ? [v1: Nat$] : (nat$(v0) = v1 & % 224.97/33.35 Nat$(v1)) & ? [v0: A_a_n_vec_a_n_vec_fun_fun$] : ? [v1: % 224.97/33.35 A_n_vec_set_nat_fun$] : (dim$(v0) = v1 & A_n_vec_set_nat_fun$(v1)) & ? [v0: % 224.97/33.35 A_a_rows_vec_a_rows_vec_fun_fun$] : ? [v1: A_rows_vec_set_nat_fun$] : % 224.97/33.35 (dim$a(v0) = v1 & A_rows_vec_set_nat_fun$(v1)) & ? [v0: Int_set$] : ? [v1: % 224.97/33.35 Int_bool_fun$] : (uub$(v0) = v1 & Int_bool_fun$(v1)) & ? [v0: int] : ? % 224.97/33.35 [v1: Int_set_bool_fun$] : (member$d(v0) = v1 & Int_set_bool_fun$(v1)) & ? % 224.97/33.35 [v0: Nat_set$] : ? [v1: Nat_bool_fun$] : (uud$(v0) = v1 & Nat_bool_fun$(v1)) % 224.97/33.35 & ? [v0: Nat$] : ? [v1: Nat_set_bool_fun$] : (member$c(v0) = v1 & % 224.97/33.35 Nat_set_bool_fun$(v1)) & ? [v0: Real_set$] : ? [v1: Real_bool_fun$] : % 224.97/33.35 (uuc$(v0) = v1 & Real_bool_fun$(v1)) & ? [v0: $real] : ? [v1: % 224.97/33.35 Real_set_bool_fun$] : (member$b(v0) = v1 & Real_set_bool_fun$(v1)) & ? [v0: % 224.97/33.35 A_n_vec_set$] : ? [v1: A_n_vec_bool_fun$] : (uu$(v0) = v1 & % 224.97/33.35 A_n_vec_bool_fun$(v1)) & ? [v0: A_n_vec$] : ? [v1: A_n_vec_set_bool_fun$] % 224.97/33.35 : (member$a(v0) = v1 & A_n_vec_set_bool_fun$(v1)) & ? [v0: A_rows_vec_set$] : % 224.97/33.35 ? [v1: A_rows_vec_bool_fun$] : (uua$(v0) = v1 & A_rows_vec_bool_fun$(v1)) % 224.97/33.35 % 224.97/33.35 Further assumptions not needed in the proof: % 224.97/33.35 -------------------------------------------- % 224.97/33.35 axiom0, axiom1, axiom100, axiom101, axiom103, axiom104, axiom105, axiom106, % 224.97/33.35 axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, axiom112, axiom113, % 224.97/33.35 axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, axiom120, axiom121, % 224.97/33.35 axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, axiom128, axiom129, % 224.97/33.35 axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, axiom135, axiom136, % 224.97/33.35 axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, axiom142, axiom143, % 224.97/33.35 axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, axiom151, % 224.97/33.35 axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, axiom158, axiom159, % 224.97/33.35 axiom16, axiom160, axiom161, axiom162, axiom163, axiom164, axiom165, axiom166, % 224.97/33.35 axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, axiom172, axiom173, % 224.97/33.35 axiom174, axiom175, axiom176, axiom178, axiom179, axiom18, axiom180, axiom181, % 224.97/33.35 axiom182, axiom183, axiom184, axiom185, axiom186, axiom187, axiom188, axiom189, % 224.97/33.35 axiom19, axiom190, axiom191, axiom192, axiom193, axiom194, axiom195, axiom196, % 224.97/33.35 axiom197, axiom198, axiom199, axiom2, axiom20, axiom200, axiom201, axiom202, % 224.97/33.35 axiom203, axiom204, axiom205, axiom206, axiom207, axiom208, axiom209, axiom21, % 224.97/33.35 axiom210, axiom211, axiom212, axiom213, axiom214, axiom215, axiom217, axiom218, % 224.97/33.35 axiom219, axiom22, axiom220, axiom221, axiom222, axiom223, axiom224, axiom225, % 224.97/33.35 axiom226, axiom227, axiom228, axiom229, axiom23, axiom230, axiom231, axiom232, % 224.97/33.35 axiom233, axiom234, axiom235, axiom236, axiom237, axiom238, axiom239, axiom24, % 224.97/33.35 axiom240, axiom241, axiom242, axiom243, axiom244, axiom245, axiom246, axiom247, % 224.97/33.35 axiom248, axiom249, axiom25, axiom250, axiom251, axiom252, axiom253, axiom254, % 224.97/33.35 axiom255, axiom256, axiom257, axiom258, axiom259, axiom26, axiom260, axiom261, % 224.97/33.35 axiom262, axiom263, axiom265, axiom266, axiom267, axiom268, axiom269, axiom270, % 224.97/33.35 axiom272, axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, % 224.97/33.35 axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, % 224.97/33.35 axiom289, axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, % 224.97/33.35 axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, % 224.97/33.35 axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, % 224.97/33.35 axiom310, axiom311, axiom312, axiom314, axiom315, axiom316, axiom317, axiom318, % 224.97/33.35 axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, axiom325, % 224.97/33.35 axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, axiom332, % 224.97/33.35 axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, % 224.97/33.35 axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, % 224.97/33.35 axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, % 224.97/33.35 axiom355, axiom356, axiom357, axiom358, axiom359, axiom360, axiom361, axiom362, % 224.97/33.35 axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, % 224.97/33.35 axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, % 224.97/33.35 axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, % 224.97/33.35 axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, axiom392, % 224.97/33.35 axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, axiom4, % 224.97/33.35 axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, axiom406, % 224.97/33.35 axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, axiom413, % 224.97/33.35 axiom414, axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, axiom420, % 224.97/33.35 axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, axiom428, % 224.97/33.35 axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, axiom435, % 224.97/33.35 axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, axiom442, % 224.97/33.35 axiom443, axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, axiom45, % 224.97/33.35 axiom450, axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, axiom457, % 224.97/33.35 axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, axiom464, % 224.97/33.35 axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, axiom471, % 224.97/33.35 axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, axiom479, axiom48, % 224.97/33.35 axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, % 224.97/33.35 axiom488, axiom489, axiom490, axiom491, axiom492, axiom493, axiom494, axiom495, % 224.97/33.35 axiom496, axiom497, axiom498, axiom499, axiom5, axiom500, axiom501, axiom502, % 224.97/33.35 axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, axiom509, axiom510, % 224.97/33.35 axiom511, axiom512, axiom513, axiom514, axiom515, axiom516, axiom517, axiom518, % 224.97/33.35 axiom519, axiom520, axiom521, axiom522, axiom523, axiom525, axiom526, axiom527, % 224.97/33.35 axiom528, axiom529, axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, % 224.97/33.35 axiom536, axiom537, axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, % 224.97/33.35 axiom543, axiom544, axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, % 224.97/33.35 axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, % 224.97/33.35 axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, axiom567, % 224.97/33.35 axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, axiom574, % 224.97/33.35 axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, % 224.97/33.35 axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, % 224.97/33.35 axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, % 224.97/33.35 axiom597, axiom598, axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, % 224.97/33.35 axiom609, axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, % 224.97/33.35 axiom616, axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, % 224.97/33.35 axiom623, axiom624, axiom625, axiom626, axiom627, axiom628, axiom63, axiom630, % 224.97/33.35 axiom631, axiom64, axiom65, axiom66, axiom67, axiom68, axiom69, axiom7, axiom70, % 224.97/33.35 axiom71, axiom72, axiom74, axiom75, axiom77, axiom78, axiom79, axiom8, axiom80, % 224.97/33.35 axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, axiom87, axiom88, axiom89, % 224.97/33.35 axiom9, axiom90, axiom91, axiom92, axiom93, axiom96, axiom97, axiom99, % 224.97/33.35 formula_633, formula_634 % 224.97/33.35 % 224.97/33.35 Those formulas are unsatisfiable: % 224.97/33.35 --------------------------------- % 224.97/33.35 % 224.97/33.35 Begin of proof % 224.97/33.35 | % 224.97/33.35 | ALPHA: (axiom10) implies: % 224.97/33.36 | (1) ? [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.97/33.36 | A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.97/33.36 | A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.97/33.36 | A_n_vec_rows_vec$(v1) | ? [v3: Nat$] : ? [v4: int] : ? [v5: any] % 224.97/33.36 | : (fun_app$k(v0, v2) = v3 & fun_app$j(of_nat$, v3) = v4 & % 224.97/33.36 | fun_app$d(finite$, v2) = v5 & Nat$(v3) & ( ~ (v5 = 0) | ~ % 224.97/33.36 | ($lesseq(1, v4)))))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom12) implies: % 224.97/33.36 | (2) ? [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.97/33.36 | A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.97/33.36 | A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.97/33.36 | A_n_vec_rows_vec$(v1) | ? [v3: any] : ? [v4: Nat$] : ? [v5: int] % 224.97/33.36 | : (fun_app$k(v0, v2) = v4 & fun_app$j(of_nat$, v4) = v5 & % 224.97/33.36 | fun_app$d(finite$, v2) = v3 & Nat$(v4) & (v3 = 0 | ~ % 224.97/33.36 | ($lesseq(v5, 0))))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom36) implies: % 224.97/33.36 | (3) ! [v0: Nat_bool_fun$] : ! [v1: Nat$] : ! [v2: int] : (v2 = 0 | ~ % 224.97/33.36 | (fun_app$g(v0, v1) = v2) | ~ Nat_bool_fun$(v0) | ~ Nat$(v1) | ? % 224.97/33.36 | [v3: Nat$] : ? [v4: int] : ? [v5: int] : ( ~ (v4 = 0) & % 224.97/33.36 | fun_app$j(of_nat$, v3) = v5 & fun_app$g(v0, v3) = v4 & Nat$(v3) & % 224.97/33.36 | ! [v6: Nat$] : ! [v7: int] : ( ~ ($lesseq(1, $difference(v5, v7))) % 224.97/33.36 | | ~ (fun_app$j(of_nat$, v6) = v7) | ~ Nat$(v6) | fun_app$g(v0, % 224.97/33.36 | v6) = 0))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom60) implies: % 224.97/33.36 | (4) ? [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.97/33.36 | A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.97/33.36 | A_n_vec_set$] : ( ~ (solution_set$(v1, zero$) = v2) | ~ % 224.97/33.36 | A_n_vec_rows_vec$(v1) | ? [v3: Nat$] : ? [v4: int] : ? [v5: % 224.97/33.36 | A_n_vec_set$] : ? [v6: Nat$] : (null_space$a(v1) = v5 & % 224.97/33.36 | fun_app$k(v0, v5) = v6 & fun_app$k(v0, v2) = v3 & % 224.97/33.36 | fun_app$j(of_nat$, v6) = v4 & fun_app$j(of_nat$, v3) = v4 & % 224.97/33.36 | Nat$(v6) & Nat$(v3) & A_n_vec_set$(v5)))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom73) implies: % 224.97/33.36 | (5) ? [v0: Nat_bool_fun$] : (fun_app$q(less$, zero$c) = v0 & % 224.97/33.36 | Nat_bool_fun$(v0) & ~ (fun_app$g(v0, zero$c) = 0) & ! [v1: Nat$] : % 224.97/33.36 | ! [v2: int] : (v2 = 0 | v1 = zero$c | ~ (fun_app$g(v0, v1) = v2) | % 224.97/33.36 | ~ Nat$(v1))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom76) implies: % 224.97/33.36 | (6) ? [v0: Nat_bool_fun$] : (fun_app$q(less$, zero$c) = v0 & % 224.97/33.36 | Nat_bool_fun$(v0) & ! [v1: Nat$] : ! [v2: int] : (v2 = 0 | v1 = % 224.97/33.36 | zero$c | ~ (fun_app$g(v0, v1) = v2) | ~ Nat$(v1))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom94) implies: % 224.97/33.36 | (7) ? [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.97/33.36 | A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec_rows_vec$] : ! [v2: % 224.97/33.36 | A_rows_vec$] : ! [v3: A_rows_vec_bool_fun$] : ( ~ % 224.97/33.36 | (consistent$a(v1) = v3) | ~ (fun_app$b(v3, v2) = 0) | ~ % 224.97/33.36 | A_n_vec_rows_vec$(v1) | ~ A_rows_vec$(v2) | ? [v4: A_n_vec_set$] % 224.97/33.36 | : ? [v5: Nat$] : ? [v6: int] : ( ~ (v6 = 0) & fun_app$k(v0, v4) = % 224.97/33.36 | v5 & fun_app$j(of_nat$, v5) = v6 & solution_set$(v1, zero$) = v4 % 224.97/33.36 | & Nat$(v5) & A_n_vec_set$(v4)) | ? [v4: A_n_vec$] : ? [v5: % 224.97/33.36 | A_rows_vec_bool_fun$] : (is_solution$a(v4, v1) = v5 & % 224.97/33.36 | fun_app$b(v5, v2) = 0 & A_n_vec$(v4) & A_rows_vec_bool_fun$(v5) & % 224.97/33.36 | ! [v6: A_n_vec$] : ! [v7: A_rows_vec_bool_fun$] : (v6 = v4 | ~ % 224.97/33.36 | (is_solution$a(v6, v1) = v7) | ~ (fun_app$b(v7, v2) = 0) | ~ % 224.97/33.36 | A_n_vec$(v6))))) % 224.97/33.36 | % 224.97/33.36 | ALPHA: (axiom95) implies: % 224.97/33.37 | (8) ? [v0: Nat_bool_fun$] : ? [v1: int] : ( ~ (v1 = 0) & fun_app$q(less$, % 224.97/33.37 | zero$c) = v0 & fun_app$g(v0, zero$c) = v1 & Nat_bool_fun$(v0)) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom98) implies: % 224.97/33.37 | (9) ? [v0: Nat_bool_fun$] : (fun_app$q(less$, zero$c) = v0 & % 224.97/33.37 | Nat_bool_fun$(v0) & ! [v1: Nat$] : ! [v2: Nat$] : ( ~ % 224.97/33.37 | (fun_app$r(of_nat$a, v1) = v2) | ~ Nat$(v1) | ? [v3: any] : ? % 224.97/33.37 | [v4: int] : (fun_app$j(of_nat$, v1) = v4 & fun_app$g(v0, v2) = v3 & % 224.97/33.37 | ( ~ (v3 = 0) | ~ ($lesseq(v4, 0)))) & ! [v1: Nat$] : ! [v2: % 224.97/33.37 | Nat$] : ( ~ (fun_app$r(of_nat$a, v1) = v2) | ~ Nat$(v1) | ? % 224.97/33.37 | [v3: int] : ? [v4: any] : (fun_app$j(of_nat$, v1) = v3 & % 224.97/33.37 | fun_app$g(v0, v2) = v4 & (v4 = 0 | ~ ($lesseq(1, v3)))))) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom102) implies: % 224.97/33.37 | (10) ? [v0: A_n_vec_set_nat_fun$] : ? [v1: Nat$] : % 224.97/33.37 | (dim$(vector_scalar_mult$) = v0 & fun_app$k(v0, bot$a) = v1 & % 224.97/33.37 | fun_app$j(of_nat$, v1) = 0 & A_n_vec_set_nat_fun$(v0) & Nat$(v1)) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom177) implies: % 224.97/33.37 | (11) fun_app$j(of_nat$, bot$g) = 0 % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom216) implies: % 224.97/33.37 | (12) ! [v0: Nat$] : ! [v1: Nat_bool_fun$] : ( ~ (fun_app$q(less$, v0) = % 224.97/33.37 | v1) | ~ Nat$(v0) | ? [v2: int] : ( ~ (v2 = 0) & fun_app$g(v1, % 224.97/33.37 | bot$g) = v2)) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom264) implies: % 224.97/33.37 | (13) ? [v0: A_n_vec_set_nat_fun$] : ? [v1: A_n_vec_set$] : % 224.97/33.37 | (insert$a(zero$a, bot$a) = v1 & dim$(vector_scalar_mult$) = v0 & % 224.97/33.37 | A_n_vec_set_nat_fun$(v0) & A_n_vec_set$(v1) & ! [v2: A_n_vec_set$] % 224.97/33.37 | : ! [v3: Nat$] : (v2 = v1 | v2 = bot$a | ~ (fun_app$k(v0, v2) = % 224.97/33.37 | v3) | ~ A_n_vec_set$(v2) | ? [v4: int] : ( ~ (v4 = 0) & % 224.97/33.37 | fun_app$j(of_nat$, v3) = v4))) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom271) implies: % 224.97/33.37 | (14) ? [v0: A_n_vec_set_nat_fun$] : (dim$(vector_scalar_mult$) = v0 & % 224.97/33.37 | A_n_vec_set_nat_fun$(v0) & ! [v1: A_n_vec$] : ! [v2: A_n_vec_set$] % 224.97/33.37 | : (v1 = zero$a | ~ (insert$a(v1, bot$a) = v2) | ~ A_n_vec$(v1) | % 224.97/33.37 | ? [v3: Nat$] : (fun_app$k(v0, v2) = v3 & fun_app$j(of_nat$, v3) = % 224.97/33.37 | 1 & Nat$(v3))) & ! [v1: A_n_vec_set$] : ( ~ (insert$a(zero$a, % 224.97/33.37 | bot$a) = v1) | ? [v2: Nat$] : (fun_app$k(v0, v1) = v2 & % 224.97/33.37 | fun_app$j(of_nat$, v2) = 0 & Nat$(v2)))) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom391) implies: % 224.97/33.37 | (15) Nat$(bot$g) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom524) implies: % 224.97/33.37 | (16) Nat$(zero$c) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (axiom629) implies: % 224.97/33.37 | (17) ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | ~ % 224.97/33.37 | (fun_app$j(of_nat$, v0) = v1) | ~ Nat$(v0)) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (conjecture6) implies: % 224.97/33.37 | (18) A_n_vec_rows_vec$(a$) % 224.97/33.37 | (19) ? [v0: A_n_vec_set$] : ? [v1: any] : ? [v2: A_n_vec_set_nat_fun$] : % 224.97/33.37 | ? [v3: Nat$] : ? [v4: int] : (dim$(vector_scalar_mult$) = v2 & % 224.97/33.37 | fun_app$k(v2, v0) = v3 & fun_app$j(of_nat$, v3) = v4 & % 224.97/33.37 | solution_set$(a$, zero$) = v0 & fun_app$d(finite$, v0) = v1 & % 224.97/33.37 | A_n_vec_set_nat_fun$(v2) & Nat$(v3) & A_n_vec_set$(v0) & ((v1 = 0 & % 224.97/33.37 | $lesseq(1, v4)) | ( ~ (v1 = 0) & $lesseq(v4, 0)))) % 224.97/33.37 | % 224.97/33.37 | ALPHA: (function-axioms) implies: % 224.97/33.37 | (20) ! [v0: A_n_vec_set_nat_fun$] : ! [v1: A_n_vec_set_nat_fun$] : ! % 224.97/33.37 | [v2: A_a_n_vec_a_n_vec_fun_fun$] : (v1 = v0 | ~ (dim$(v2) = v1) | ~ % 224.97/33.37 | (dim$(v2) = v0)) % 224.97/33.37 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 224.97/33.37 | A_n_vec_set$] : ! [v3: A_n_vec_set_bool_fun$] : (v1 = v0 | ~ % 224.97/33.37 | (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) % 224.97/33.37 | (22) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 224.97/33.37 | Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$g(v3, v2) = % 224.97/33.37 | v1) | ~ (fun_app$g(v3, v2) = v0)) % 224.97/33.38 | (23) ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : ! [v3: Nat_int_fun$] : % 224.97/33.38 | (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) % 224.97/33.38 | (24) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_n_vec_set$] : ! [v3: % 224.97/33.38 | A_n_vec_set_nat_fun$] : (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | ~ % 224.97/33.38 | (fun_app$k(v3, v2) = v0)) % 224.97/33.38 | (25) ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : ! % 224.97/33.38 | [v3: Nat_nat_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | % 224.97/33.38 | ~ (fun_app$q(v3, v2) = v0)) % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (8) with fresh symbols all_743_0, all_743_1 gives: % 224.97/33.38 | (26) ~ (all_743_0 = 0) & fun_app$q(less$, zero$c) = all_743_1 & % 224.97/33.38 | fun_app$g(all_743_1, zero$c) = all_743_0 & Nat_bool_fun$(all_743_1) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (26) implies: % 224.97/33.38 | (27) ~ (all_743_0 = 0) % 224.97/33.38 | (28) fun_app$g(all_743_1, zero$c) = all_743_0 % 224.97/33.38 | (29) fun_app$q(less$, zero$c) = all_743_1 % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (10) with fresh symbols all_775_0, all_775_1 gives: % 224.97/33.38 | (30) dim$(vector_scalar_mult$) = all_775_1 & fun_app$k(all_775_1, bot$a) = % 224.97/33.38 | all_775_0 & fun_app$j(of_nat$, all_775_0) = 0 & % 224.97/33.38 | A_n_vec_set_nat_fun$(all_775_1) & Nat$(all_775_0) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (30) implies: % 224.97/33.38 | (31) dim$(vector_scalar_mult$) = all_775_1 % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (6) with fresh symbol all_786_0 gives: % 224.97/33.38 | (32) fun_app$q(less$, zero$c) = all_786_0 & Nat_bool_fun$(all_786_0) & ! % 224.97/33.38 | [v0: Nat$] : ! [v1: int] : (v1 = 0 | v0 = zero$c | ~ % 224.97/33.38 | (fun_app$g(all_786_0, v0) = v1) | ~ Nat$(v0)) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (32) implies: % 224.97/33.38 | (33) Nat_bool_fun$(all_786_0) % 224.97/33.38 | (34) fun_app$q(less$, zero$c) = all_786_0 % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (5) with fresh symbol all_797_0 gives: % 224.97/33.38 | (35) fun_app$q(less$, zero$c) = all_797_0 & Nat_bool_fun$(all_797_0) & ~ % 224.97/33.38 | (fun_app$g(all_797_0, zero$c) = 0) & ! [v0: Nat$] : ! [v1: int] : % 224.97/33.38 | (v1 = 0 | v0 = zero$c | ~ (fun_app$g(all_797_0, v0) = v1) | ~ % 224.97/33.38 | Nat$(v0)) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (35) implies: % 224.97/33.38 | (36) fun_app$q(less$, zero$c) = all_797_0 % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (5) with fresh symbol all_800_0 gives: % 224.97/33.38 | (37) fun_app$q(less$, zero$c) = all_800_0 & Nat_bool_fun$(all_800_0) & ~ % 224.97/33.38 | (fun_app$g(all_800_0, zero$c) = 0) & ! [v0: Nat$] : ! [v1: int] : % 224.97/33.38 | (v1 = 0 | v0 = zero$c | ~ (fun_app$g(all_800_0, v0) = v1) | ~ % 224.97/33.38 | Nat$(v0)) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (37) implies: % 224.97/33.38 | (38) fun_app$q(less$, zero$c) = all_800_0 % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (1) with fresh symbol all_815_0 gives: % 224.97/33.38 | (39) dim$(vector_scalar_mult$) = all_815_0 & % 224.97/33.38 | A_n_vec_set_nat_fun$(all_815_0) & ! [v0: A_n_vec_rows_vec$] : ! [v1: % 224.97/33.38 | A_n_vec_set$] : ( ~ (solution_set$(v0, zero$) = v1) | ~ % 224.97/33.38 | A_n_vec_rows_vec$(v0) | ? [v2: Nat$] : ? [v3: int] : ? [v4: any] % 224.97/33.38 | : (fun_app$k(all_815_0, v1) = v2 & fun_app$j(of_nat$, v2) = v3 & % 224.97/33.38 | fun_app$d(finite$, v1) = v4 & Nat$(v2) & ( ~ (v4 = 0) | ~ % 224.97/33.38 | ($lesseq(1, v3))))) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (39) implies: % 224.97/33.38 | (40) dim$(vector_scalar_mult$) = all_815_0 % 224.97/33.38 | (41) ! [v0: A_n_vec_rows_vec$] : ! [v1: A_n_vec_set$] : ( ~ % 224.97/33.38 | (solution_set$(v0, zero$) = v1) | ~ A_n_vec_rows_vec$(v0) | ? [v2: % 224.97/33.38 | Nat$] : ? [v3: int] : ? [v4: any] : (fun_app$k(all_815_0, v1) = % 224.97/33.38 | v2 & fun_app$j(of_nat$, v2) = v3 & fun_app$d(finite$, v1) = v4 & % 224.97/33.38 | Nat$(v2) & ( ~ (v4 = 0) | ~ ($lesseq(1, v3))))) % 224.97/33.38 | % 224.97/33.38 | DELTA: instantiating (2) with fresh symbol all_818_0 gives: % 224.97/33.38 | (42) dim$(vector_scalar_mult$) = all_818_0 & % 224.97/33.38 | A_n_vec_set_nat_fun$(all_818_0) & ! [v0: A_n_vec_rows_vec$] : ! [v1: % 224.97/33.38 | A_n_vec_set$] : ( ~ (solution_set$(v0, zero$) = v1) | ~ % 224.97/33.38 | A_n_vec_rows_vec$(v0) | ? [v2: any] : ? [v3: Nat$] : ? [v4: int] % 224.97/33.38 | : (fun_app$k(all_818_0, v1) = v3 & fun_app$j(of_nat$, v3) = v4 & % 224.97/33.38 | fun_app$d(finite$, v1) = v2 & Nat$(v3) & (v2 = 0 | ~ ($lesseq(v4, % 224.97/33.38 | 0)))) % 224.97/33.38 | % 224.97/33.38 | ALPHA: (42) implies: % 224.97/33.38 | (43) dim$(vector_scalar_mult$) = all_818_0 % 224.97/33.39 | (44) ! [v0: A_n_vec_rows_vec$] : ! [v1: A_n_vec_set$] : ( ~ % 224.97/33.39 | (solution_set$(v0, zero$) = v1) | ~ A_n_vec_rows_vec$(v0) | ? [v2: % 224.97/33.39 | any] : ? [v3: Nat$] : ? [v4: int] : (fun_app$k(all_818_0, v1) = % 224.97/33.39 | v3 & fun_app$j(of_nat$, v3) = v4 & fun_app$d(finite$, v1) = v2 & % 224.97/33.39 | Nat$(v3) & (v2 = 0 | ~ ($lesseq(v4, 0)))) % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (13) with fresh symbols all_824_0, all_824_1 gives: % 224.97/33.39 | (45) insert$a(zero$a, bot$a) = all_824_0 & dim$(vector_scalar_mult$) = % 224.97/33.39 | all_824_1 & A_n_vec_set_nat_fun$(all_824_1) & A_n_vec_set$(all_824_0) % 224.97/33.39 | & ! [v0: any] : ! [v1: Nat$] : (v0 = all_824_0 | v0 = bot$a | ~ % 224.97/33.39 | (fun_app$k(all_824_1, v0) = v1) | ~ A_n_vec_set$(v0) | ? [v2: int] % 224.97/33.39 | : ( ~ (v2 = 0) & fun_app$j(of_nat$, v1) = v2)) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (45) implies: % 224.97/33.39 | (46) dim$(vector_scalar_mult$) = all_824_1 % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (14) with fresh symbol all_833_0 gives: % 224.97/33.39 | (47) dim$(vector_scalar_mult$) = all_833_0 & % 224.97/33.39 | A_n_vec_set_nat_fun$(all_833_0) & ! [v0: A_n_vec$] : ! [v1: % 224.97/33.39 | A_n_vec_set$] : (v0 = zero$a | ~ (insert$a(v0, bot$a) = v1) | ~ % 224.97/33.39 | A_n_vec$(v0) | ? [v2: Nat$] : (fun_app$k(all_833_0, v1) = v2 & % 224.97/33.39 | fun_app$j(of_nat$, v2) = 1 & Nat$(v2))) & ! [v0: A_n_vec_set$] : % 224.97/33.39 | ( ~ (insert$a(zero$a, bot$a) = v0) | ? [v1: Nat$] : % 224.97/33.39 | (fun_app$k(all_833_0, v0) = v1 & fun_app$j(of_nat$, v1) = 0 & % 224.97/33.39 | Nat$(v1))) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (47) implies: % 224.97/33.39 | (48) dim$(vector_scalar_mult$) = all_833_0 % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (19) with fresh symbols all_836_0, all_836_1, all_836_2, % 224.97/33.39 | all_836_3, all_836_4 gives: % 224.97/33.39 | (49) dim$(vector_scalar_mult$) = all_836_2 & fun_app$k(all_836_2, % 224.97/33.39 | all_836_4) = all_836_1 & fun_app$j(of_nat$, all_836_1) = all_836_0 & % 224.97/33.39 | solution_set$(a$, zero$) = all_836_4 & fun_app$d(finite$, all_836_4) = % 224.97/33.39 | all_836_3 & A_n_vec_set_nat_fun$(all_836_2) & Nat$(all_836_1) & % 224.97/33.39 | A_n_vec_set$(all_836_4) & ((all_836_3 = 0 & $lesseq(1, all_836_0)) | ( % 224.97/33.39 | ~ (all_836_3 = 0) & $lesseq(all_836_0, 0))) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (49) implies: % 224.97/33.39 | (50) Nat$(all_836_1) % 224.97/33.39 | (51) fun_app$d(finite$, all_836_4) = all_836_3 % 224.97/33.39 | (52) solution_set$(a$, zero$) = all_836_4 % 224.97/33.39 | (53) fun_app$j(of_nat$, all_836_1) = all_836_0 % 224.97/33.39 | (54) fun_app$k(all_836_2, all_836_4) = all_836_1 % 224.97/33.39 | (55) dim$(vector_scalar_mult$) = all_836_2 % 224.97/33.39 | (56) (all_836_3 = 0 & $lesseq(1, all_836_0)) | ( ~ (all_836_3 = 0) & % 224.97/33.39 | $lesseq(all_836_0, 0)) % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (4) with fresh symbol all_838_0 gives: % 224.97/33.39 | (57) dim$(vector_scalar_mult$) = all_838_0 & % 224.97/33.39 | A_n_vec_set_nat_fun$(all_838_0) & ! [v0: A_n_vec_rows_vec$] : ! [v1: % 224.97/33.39 | A_n_vec_set$] : ( ~ (solution_set$(v0, zero$) = v1) | ~ % 224.97/33.39 | A_n_vec_rows_vec$(v0) | ? [v2: Nat$] : ? [v3: int] : ? [v4: % 224.97/33.39 | A_n_vec_set$] : ? [v5: Nat$] : (null_space$a(v0) = v4 & % 224.97/33.39 | fun_app$k(all_838_0, v4) = v5 & fun_app$k(all_838_0, v1) = v2 & % 224.97/33.39 | fun_app$j(of_nat$, v5) = v3 & fun_app$j(of_nat$, v2) = v3 & % 224.97/33.39 | Nat$(v5) & Nat$(v2) & A_n_vec_set$(v4))) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (57) implies: % 224.97/33.39 | (58) dim$(vector_scalar_mult$) = all_838_0 % 224.97/33.39 | (59) ! [v0: A_n_vec_rows_vec$] : ! [v1: A_n_vec_set$] : ( ~ % 224.97/33.39 | (solution_set$(v0, zero$) = v1) | ~ A_n_vec_rows_vec$(v0) | ? [v2: % 224.97/33.39 | Nat$] : ? [v3: int] : ? [v4: A_n_vec_set$] : ? [v5: Nat$] : % 224.97/33.39 | (null_space$a(v0) = v4 & fun_app$k(all_838_0, v4) = v5 & % 224.97/33.39 | fun_app$k(all_838_0, v1) = v2 & fun_app$j(of_nat$, v5) = v3 & % 224.97/33.39 | fun_app$j(of_nat$, v2) = v3 & Nat$(v5) & Nat$(v2) & % 224.97/33.39 | A_n_vec_set$(v4))) % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (9) with fresh symbol all_850_0 gives: % 224.97/33.39 | (60) fun_app$q(less$, zero$c) = all_850_0 & Nat_bool_fun$(all_850_0) & ! % 224.97/33.39 | [v0: Nat$] : ! [v1: Nat$] : ( ~ (fun_app$r(of_nat$a, v0) = v1) | ~ % 224.97/33.39 | Nat$(v0) | ? [v2: any] : ? [v3: int] : (fun_app$j(of_nat$, v0) = % 224.97/33.39 | v3 & fun_app$g(all_850_0, v1) = v2 & ( ~ (v2 = 0) | ~ % 224.97/33.39 | ($lesseq(v3, 0)))) & ! [v0: Nat$] : ! [v1: Nat$] : ( ~ % 224.97/33.39 | (fun_app$r(of_nat$a, v0) = v1) | ~ Nat$(v0) | ? [v2: int] : ? % 224.97/33.39 | [v3: any] : (fun_app$j(of_nat$, v0) = v2 & fun_app$g(all_850_0, % 224.97/33.39 | v1) = v3 & (v3 = 0 | ~ ($lesseq(1, v2))))) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (60) implies: % 224.97/33.39 | (61) fun_app$q(less$, zero$c) = all_850_0 % 224.97/33.39 | % 224.97/33.39 | DELTA: instantiating (7) with fresh symbol all_875_0 gives: % 224.97/33.39 | (62) dim$(vector_scalar_mult$) = all_875_0 & % 224.97/33.39 | A_n_vec_set_nat_fun$(all_875_0) & ! [v0: A_n_vec_rows_vec$] : ! [v1: % 224.97/33.39 | A_rows_vec$] : ! [v2: A_rows_vec_bool_fun$] : ( ~ (consistent$a(v0) % 224.97/33.39 | = v2) | ~ (fun_app$b(v2, v1) = 0) | ~ A_n_vec_rows_vec$(v0) | ~ % 224.97/33.39 | A_rows_vec$(v1) | ? [v3: A_n_vec_set$] : ? [v4: Nat$] : ? [v5: % 224.97/33.39 | int] : ( ~ (v5 = 0) & fun_app$k(all_875_0, v3) = v4 & % 224.97/33.39 | fun_app$j(of_nat$, v4) = v5 & solution_set$(v0, zero$) = v3 & % 224.97/33.39 | Nat$(v4) & A_n_vec_set$(v3)) | ? [v3: A_n_vec$] : ? [v4: % 224.97/33.39 | A_rows_vec_bool_fun$] : (is_solution$a(v3, v0) = v4 & % 224.97/33.39 | fun_app$b(v4, v1) = 0 & A_n_vec$(v3) & A_rows_vec_bool_fun$(v4) & % 224.97/33.39 | ! [v5: A_n_vec$] : ! [v6: A_rows_vec_bool_fun$] : (v5 = v3 | ~ % 224.97/33.39 | (is_solution$a(v5, v0) = v6) | ~ (fun_app$b(v6, v1) = 0) | ~ % 224.97/33.39 | A_n_vec$(v5)))) % 224.97/33.39 | % 224.97/33.39 | ALPHA: (62) implies: % 224.97/33.39 | (63) dim$(vector_scalar_mult$) = all_875_0 % 224.97/33.39 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_833_0, all_836_2, % 224.97/33.40 | vector_scalar_mult$, simplifying with (48), (55) gives: % 224.97/33.40 | (64) all_836_2 = all_833_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_818_0, all_836_2, % 224.97/33.40 | vector_scalar_mult$, simplifying with (43), (55) gives: % 224.97/33.40 | (65) all_836_2 = all_818_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_775_1, all_836_2, % 224.97/33.40 | vector_scalar_mult$, simplifying with (31), (55) gives: % 224.97/33.40 | (66) all_836_2 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_818_0, all_838_0, % 224.97/33.40 | vector_scalar_mult$, simplifying with (43), (58) gives: % 224.97/33.40 | (67) all_838_0 = all_818_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_815_0, all_838_0, % 224.97/33.40 | vector_scalar_mult$, simplifying with (40), (58) gives: % 224.97/33.40 | (68) all_838_0 = all_815_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_836_2, all_875_0, % 224.97/33.40 | vector_scalar_mult$, simplifying with (55), (63) gives: % 224.97/33.40 | (69) all_875_0 = all_836_2 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (20) with all_824_1, all_875_0, % 224.97/33.40 | vector_scalar_mult$, simplifying with (46), (63) gives: % 224.97/33.40 | (70) all_875_0 = all_824_1 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (25) with all_743_1, all_800_0, zero$c, less$, % 224.97/33.40 | simplifying with (29), (38) gives: % 224.97/33.40 | (71) all_800_0 = all_743_1 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (25) with all_800_0, all_850_0, zero$c, less$, % 224.97/33.40 | simplifying with (38), (61) gives: % 224.97/33.40 | (72) all_850_0 = all_800_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (25) with all_797_0, all_850_0, zero$c, less$, % 224.97/33.40 | simplifying with (36), (61) gives: % 224.97/33.40 | (73) all_850_0 = all_797_0 % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (25) with all_786_0, all_850_0, zero$c, less$, % 224.97/33.40 | simplifying with (34), (61) gives: % 224.97/33.40 | (74) all_850_0 = all_786_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (69), (70) imply: % 224.97/33.40 | (75) all_836_2 = all_824_1 % 224.97/33.40 | % 224.97/33.40 | SIMP: (75) implies: % 224.97/33.40 | (76) all_836_2 = all_824_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (72), (73) imply: % 224.97/33.40 | (77) all_800_0 = all_797_0 % 224.97/33.40 | % 224.97/33.40 | SIMP: (77) implies: % 224.97/33.40 | (78) all_800_0 = all_797_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (73), (74) imply: % 224.97/33.40 | (79) all_797_0 = all_786_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (67), (68) imply: % 224.97/33.40 | (80) all_818_0 = all_815_0 % 224.97/33.40 | % 224.97/33.40 | SIMP: (80) implies: % 224.97/33.40 | (81) all_818_0 = all_815_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (64), (66) imply: % 224.97/33.40 | (82) all_833_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (64), (65) imply: % 224.97/33.40 | (83) all_833_0 = all_818_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (64), (76) imply: % 224.97/33.40 | (84) all_833_0 = all_824_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (82), (84) imply: % 224.97/33.40 | (85) all_824_1 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (83), (84) imply: % 224.97/33.40 | (86) all_824_1 = all_818_0 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (85), (86) imply: % 224.97/33.40 | (87) all_818_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | SIMP: (87) implies: % 224.97/33.40 | (88) all_818_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (81), (88) imply: % 224.97/33.40 | (89) all_815_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | SIMP: (89) implies: % 224.97/33.40 | (90) all_815_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (71), (78) imply: % 224.97/33.40 | (91) all_797_0 = all_743_1 % 224.97/33.40 | % 224.97/33.40 | SIMP: (91) implies: % 224.97/33.40 | (92) all_797_0 = all_743_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (79), (92) imply: % 224.97/33.40 | (93) all_786_0 = all_743_1 % 224.97/33.40 | % 224.97/33.40 | COMBINE_EQS: (68), (90) imply: % 224.97/33.40 | (94) all_838_0 = all_775_1 % 224.97/33.40 | % 224.97/33.40 | REDUCE: (54), (66) imply: % 224.97/33.40 | (95) fun_app$k(all_775_1, all_836_4) = all_836_1 % 224.97/33.40 | % 224.97/33.40 | REDUCE: (33), (93) imply: % 224.97/33.40 | (96) Nat_bool_fun$(all_743_1) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (3) with all_743_1, zero$c, all_743_0, simplifying % 224.97/33.40 | with (16), (28), (96) gives: % 224.97/33.40 | (97) all_743_0 = 0 | ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : ( ~ (v1 % 224.97/33.40 | = 0) & fun_app$j(of_nat$, v0) = v2 & fun_app$g(all_743_1, v0) = v1 % 224.97/33.40 | & Nat$(v0) & ! [v3: Nat$] : ! [v4: int] : ( ~ ($lesseq(1, % 224.97/33.40 | $difference(v2, v4))) | ~ (fun_app$j(of_nat$, v3) = v4) | ~ % 224.97/33.40 | Nat$(v3) | fun_app$g(all_743_1, v3) = 0)) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (59) with a$, all_836_4, simplifying with (18), % 224.97/33.40 | (52) gives: % 224.97/33.40 | (98) ? [v0: Nat$] : ? [v1: int] : ? [v2: A_n_vec_set$] : ? [v3: Nat$] : % 224.97/33.40 | (null_space$a(a$) = v2 & fun_app$k(all_838_0, v2) = v3 & % 224.97/33.40 | fun_app$k(all_838_0, all_836_4) = v0 & fun_app$j(of_nat$, v3) = v1 & % 224.97/33.40 | fun_app$j(of_nat$, v0) = v1 & Nat$(v3) & Nat$(v0) & % 224.97/33.40 | A_n_vec_set$(v2)) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (44) with a$, all_836_4, simplifying with (18), % 224.97/33.40 | (52) gives: % 224.97/33.40 | (99) ? [v0: any] : ? [v1: Nat$] : ? [v2: int] : (fun_app$k(all_818_0, % 224.97/33.40 | all_836_4) = v1 & fun_app$j(of_nat$, v1) = v2 & fun_app$d(finite$, % 224.97/33.40 | all_836_4) = v0 & Nat$(v1) & (v0 = 0 | ~ ($lesseq(v2, 0))) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (41) with a$, all_836_4, simplifying with (18), % 224.97/33.40 | (52) gives: % 224.97/33.40 | (100) ? [v0: Nat$] : ? [v1: int] : ? [v2: any] : (fun_app$k(all_815_0, % 224.97/33.40 | all_836_4) = v0 & fun_app$j(of_nat$, v0) = v1 & % 224.97/33.40 | fun_app$d(finite$, all_836_4) = v2 & Nat$(v0) & ( ~ (v2 = 0) | ~ % 224.97/33.40 | ($lesseq(1, v1)))) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (17) with all_836_1, all_836_0, simplifying with % 224.97/33.40 | (50), (53) gives: % 224.97/33.40 | (101) $lesseq(0, all_836_0) % 224.97/33.40 | % 224.97/33.40 | GROUND_INST: instantiating (12) with zero$c, all_743_1, simplifying with (16), % 224.97/33.40 | (29) gives: % 224.97/33.41 | (102) ? [v0: int] : ( ~ (v0 = 0) & fun_app$g(all_743_1, bot$g) = v0) % 224.97/33.41 | % 224.97/33.41 | DELTA: instantiating (102) with fresh symbol all_957_0 gives: % 224.97/33.41 | (103) ~ (all_957_0 = 0) & fun_app$g(all_743_1, bot$g) = all_957_0 % 224.97/33.41 | % 224.97/33.41 | ALPHA: (103) implies: % 224.97/33.41 | (104) ~ (all_957_0 = 0) % 224.97/33.41 | (105) fun_app$g(all_743_1, bot$g) = all_957_0 % 224.97/33.41 | % 224.97/33.41 | DELTA: instantiating (100) with fresh symbols all_1087_0, all_1087_1, % 224.97/33.41 | all_1087_2 gives: % 224.97/33.41 | (106) fun_app$k(all_815_0, all_836_4) = all_1087_2 & fun_app$j(of_nat$, % 224.97/33.41 | all_1087_2) = all_1087_1 & fun_app$d(finite$, all_836_4) = % 224.97/33.41 | all_1087_0 & Nat$(all_1087_2) & ( ~ (all_1087_0 = 0) | ~ ($lesseq(1, % 224.97/33.41 | all_1087_1))) % 224.97/33.41 | % 224.97/33.41 | ALPHA: (106) implies: % 224.97/33.41 | (107) fun_app$d(finite$, all_836_4) = all_1087_0 % 224.97/33.41 | (108) fun_app$j(of_nat$, all_1087_2) = all_1087_1 % 224.97/33.41 | (109) fun_app$k(all_815_0, all_836_4) = all_1087_2 % 224.97/33.41 | (110) ~ (all_1087_0 = 0) | ~ ($lesseq(1, all_1087_1)) % 224.97/33.41 | % 224.97/33.41 | DELTA: instantiating (99) with fresh symbols all_1089_0, all_1089_1, % 224.97/33.41 | all_1089_2 gives: % 224.97/33.41 | (111) fun_app$k(all_818_0, all_836_4) = all_1089_1 & fun_app$j(of_nat$, % 224.97/33.41 | all_1089_1) = all_1089_0 & fun_app$d(finite$, all_836_4) = % 224.97/33.41 | all_1089_2 & Nat$(all_1089_1) & (all_1089_2 = 0 | ~ % 224.97/33.41 | ($lesseq(all_1089_0, 0)) % 224.97/33.41 | % 224.97/33.41 | ALPHA: (111) implies: % 224.97/33.41 | (112) fun_app$d(finite$, all_836_4) = all_1089_2 % 224.97/33.41 | (113) fun_app$j(of_nat$, all_1089_1) = all_1089_0 % 224.97/33.41 | (114) fun_app$k(all_818_0, all_836_4) = all_1089_1 % 224.97/33.41 | (115) all_1089_2 = 0 | ~ ($lesseq(all_1089_0, 0) % 224.97/33.41 | % 224.97/33.41 | DELTA: instantiating (98) with fresh symbols all_1103_0, all_1103_1, % 224.97/33.41 | all_1103_2, all_1103_3 gives: % 224.97/33.41 | (116) null_space$a(a$) = all_1103_1 & fun_app$k(all_838_0, all_1103_1) = % 224.97/33.41 | all_1103_0 & fun_app$k(all_838_0, all_836_4) = all_1103_3 & % 224.97/33.41 | fun_app$j(of_nat$, all_1103_0) = all_1103_2 & fun_app$j(of_nat$, % 224.97/33.41 | all_1103_3) = all_1103_2 & Nat$(all_1103_0) & Nat$(all_1103_3) & % 224.97/33.41 | A_n_vec_set$(all_1103_1) % 224.97/33.41 | % 224.97/33.41 | ALPHA: (116) implies: % 224.97/33.41 | (117) fun_app$j(of_nat$, all_1103_3) = all_1103_2 % 224.97/33.41 | (118) fun_app$k(all_838_0, all_836_4) = all_1103_3 % 224.97/33.41 | % 224.97/33.41 | REDUCE: (94), (118) imply: % 224.97/33.41 | (119) fun_app$k(all_775_1, all_836_4) = all_1103_3 % 224.97/33.41 | % 224.97/33.41 | REDUCE: (88), (114) imply: % 224.97/33.41 | (120) fun_app$k(all_775_1, all_836_4) = all_1089_1 % 224.97/33.41 | % 224.97/33.41 | REDUCE: (90), (109) imply: % 224.97/33.41 | (121) fun_app$k(all_775_1, all_836_4) = all_1087_2 % 224.97/33.41 | % 224.97/33.41 | BETA: splitting (97) gives: % 224.97/33.41 | % 224.97/33.41 | Case 1: % 224.97/33.41 | | % 224.97/33.41 | | (122) all_743_0 = 0 % 224.97/33.41 | | % 224.97/33.41 | | REDUCE: (27), (122) imply: % 224.97/33.41 | | (123) $false % 224.97/33.41 | | % 224.97/33.41 | | CLOSE: (123) is inconsistent. % 224.97/33.41 | | % 224.97/33.41 | Case 2: % 224.97/33.41 | | % 224.97/33.41 | | (124) ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : ( ~ (v1 = 0) & % 224.97/33.41 | | fun_app$j(of_nat$, v0) = v2 & fun_app$g(all_743_1, v0) = v1 & % 224.97/33.41 | | Nat$(v0) & ! [v3: Nat$] : ! [v4: int] : ( ~ ($lesseq(1, % 224.97/33.41 | | $difference(v2, v4))) | ~ (fun_app$j(of_nat$, v3) = v4) | % 224.97/33.41 | | ~ Nat$(v3) | fun_app$g(all_743_1, v3) = 0)) % 224.97/33.41 | | % 224.97/33.41 | | DELTA: instantiating (124) with fresh symbols all_1156_0, all_1156_1, % 224.97/33.41 | | all_1156_2 gives: % 224.97/33.41 | | (125) ~ (all_1156_1 = 0) & fun_app$j(of_nat$, all_1156_2) = all_1156_0 & % 224.97/33.41 | | fun_app$g(all_743_1, all_1156_2) = all_1156_1 & Nat$(all_1156_2) & % 224.97/33.41 | | ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(1, % 224.97/33.41 | | $difference(all_1156_0, v1))) | ~ (fun_app$j(of_nat$, v0) = % 224.97/33.41 | | v1) | ~ Nat$(v0) | fun_app$g(all_743_1, v0) = 0) % 224.97/33.41 | | % 224.97/33.41 | | ALPHA: (125) implies: % 224.97/33.41 | | (126) ! [v0: Nat$] : ! [v1: int] : ( ~ ($lesseq(1, % 224.97/33.41 | | $difference(all_1156_0, v1))) | ~ (fun_app$j(of_nat$, v0) = % 224.97/33.41 | | v1) | ~ Nat$(v0) | fun_app$g(all_743_1, v0) = 0) % 224.97/33.41 | | % 224.97/33.41 | | GROUND_INST: instantiating (126) with bot$g, 0, simplifying with (11), (15) % 224.97/33.41 | | gives: % 224.97/33.41 | | (127) ~ ($lesseq(1, all_1156_0)) | fun_app$g(all_743_1, bot$g) = 0 % 224.97/33.41 | | % 224.97/33.41 | | BETA: splitting (127) gives: % 224.97/33.41 | | % 224.97/33.41 | | Case 1: % 224.97/33.41 | | | % 224.97/33.41 | | | (128) fun_app$g(all_743_1, bot$g) = 0 % 224.97/33.41 | | | % 224.97/33.41 | | | GROUND_INST: instantiating (22) with 0, all_957_0, bot$g, all_743_1, % 224.97/33.41 | | | simplifying with (105), (128) gives: % 224.97/33.41 | | | (129) all_957_0 = 0 % 224.97/33.41 | | | % 224.97/33.41 | | | REDUCE: (104), (129) imply: % 224.97/33.41 | | | (130) $false % 224.97/33.41 | | | % 224.97/33.41 | | | CLOSE: (130) is inconsistent. % 224.97/33.41 | | | % 224.97/33.41 | | Case 2: % 224.97/33.41 | | | % 224.97/33.41 | | | % 224.97/33.41 | | | GROUND_INST: instantiating (21) with all_836_3, all_1089_2, all_836_4, % 224.97/33.41 | | | finite$, simplifying with (51), (112) gives: % 224.97/33.41 | | | (131) all_1089_2 = all_836_3 % 224.97/33.41 | | | % 224.97/33.41 | | | GROUND_INST: instantiating (21) with all_1087_0, all_1089_2, all_836_4, % 224.97/33.41 | | | finite$, simplifying with (107), (112) gives: % 224.97/33.41 | | | (132) all_1089_2 = all_1087_0 % 224.97/33.41 | | | % 224.97/33.41 | | | GROUND_INST: instantiating (24) with all_836_1, all_1089_1, all_836_4, % 224.97/33.41 | | | all_775_1, simplifying with (95), (120) gives: % 224.97/33.41 | | | (133) all_1089_1 = all_836_1 % 224.97/33.41 | | | % 224.97/33.41 | | | GROUND_INST: instantiating (24) with all_1089_1, all_1103_3, all_836_4, % 224.97/33.41 | | | all_775_1, simplifying with (119), (120) gives: % 224.97/33.42 | | | (134) all_1103_3 = all_1089_1 % 224.97/33.42 | | | % 224.97/33.42 | | | GROUND_INST: instantiating (24) with all_1087_2, all_1103_3, all_836_4, % 224.97/33.42 | | | all_775_1, simplifying with (119), (121) gives: % 224.97/33.42 | | | (135) all_1103_3 = all_1087_2 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (134), (135) imply: % 224.97/33.42 | | | (136) all_1089_1 = all_1087_2 % 224.97/33.42 | | | % 224.97/33.42 | | | SIMP: (136) implies: % 224.97/33.42 | | | (137) all_1089_1 = all_1087_2 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (133), (137) imply: % 224.97/33.42 | | | (138) all_1087_2 = all_836_1 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (131), (132) imply: % 224.97/33.42 | | | (139) all_1087_0 = all_836_3 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (135), (138) imply: % 224.97/33.42 | | | (140) all_1103_3 = all_836_1 % 224.97/33.42 | | | % 224.97/33.42 | | | REDUCE: (117), (140) imply: % 224.97/33.42 | | | (141) fun_app$j(of_nat$, all_836_1) = all_1103_2 % 224.97/33.42 | | | % 224.97/33.42 | | | REDUCE: (113), (133) imply: % 224.97/33.42 | | | (142) fun_app$j(of_nat$, all_836_1) = all_1089_0 % 224.97/33.42 | | | % 224.97/33.42 | | | REDUCE: (108), (138) imply: % 224.97/33.42 | | | (143) fun_app$j(of_nat$, all_836_1) = all_1087_1 % 224.97/33.42 | | | % 224.97/33.42 | | | GROUND_INST: instantiating (23) with all_836_0, all_1103_2, all_836_1, % 224.97/33.42 | | | of_nat$, simplifying with (53), (141) gives: % 224.97/33.42 | | | (144) all_1103_2 = all_836_0 % 224.97/33.42 | | | % 224.97/33.42 | | | GROUND_INST: instantiating (23) with all_1089_0, all_1103_2, all_836_1, % 224.97/33.42 | | | of_nat$, simplifying with (141), (142) gives: % 224.97/33.42 | | | (145) all_1103_2 = all_1089_0 % 224.97/33.42 | | | % 224.97/33.42 | | | GROUND_INST: instantiating (23) with all_1087_1, all_1103_2, all_836_1, % 224.97/33.42 | | | of_nat$, simplifying with (141), (143) gives: % 224.97/33.42 | | | (146) all_1103_2 = all_1087_1 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (144), (145) imply: % 224.97/33.42 | | | (147) all_1089_0 = all_836_0 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (145), (146) imply: % 224.97/33.42 | | | (148) all_1089_0 = all_1087_1 % 224.97/33.42 | | | % 224.97/33.42 | | | COMBINE_EQS: (147), (148) imply: % 224.97/33.42 | | | (149) all_1087_1 = all_836_0 % 224.97/33.42 | | | % 224.97/33.42 | | | BETA: splitting (56) gives: % 224.97/33.42 | | | % 224.97/33.42 | | | Case 1: % 224.97/33.42 | | | | % 224.97/33.42 | | | | (150) all_836_3 = 0 & $lesseq(1, all_836_0) % 224.97/33.42 | | | | % 224.97/33.42 | | | | ALPHA: (150) implies: % 224.97/33.42 | | | | (151) all_836_3 = 0 % 224.97/33.42 | | | | (152) $lesseq(1, all_836_0) % 224.97/33.42 | | | | % 224.97/33.42 | | | | COMBINE_EQS: (139), (151) imply: % 224.97/33.42 | | | | (153) all_1087_0 = 0 % 224.97/33.42 | | | | % 224.97/33.42 | | | | BETA: splitting (110) gives: % 224.97/33.42 | | | | % 224.97/33.42 | | | | Case 1: % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | (154) ~ (all_1087_0 = 0) % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | REDUCE: (153), (154) imply: % 224.97/33.42 | | | | | (155) $false % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | CLOSE: (155) is inconsistent. % 224.97/33.42 | | | | | % 224.97/33.42 | | | | Case 2: % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | (156) $lesseq(all_1087_1, 0) % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | REDUCE: (149), (156) imply: % 224.97/33.42 | | | | | (157) $lesseq(all_836_0, 0) % 224.97/33.42 | | | | | % 224.97/33.42 | | | | | COMBINE_INEQS: (152), (157) imply: % 225.28/33.42 | | | | | (158) $false % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | CLOSE: (158) is inconsistent. % 225.28/33.42 | | | | | % 225.28/33.42 | | | | End of split % 225.28/33.42 | | | | % 225.28/33.42 | | | Case 2: % 225.28/33.42 | | | | % 225.28/33.42 | | | | (159) ~ (all_836_3 = 0) & $lesseq(all_836_0, 0) % 225.28/33.42 | | | | % 225.28/33.42 | | | | ALPHA: (159) implies: % 225.28/33.42 | | | | (160) ~ (all_836_3 = 0) % 225.28/33.42 | | | | (161) $lesseq(all_836_0, 0) % 225.28/33.42 | | | | % 225.28/33.42 | | | | ANTI_SYMM: (101), (161) imply: % 225.28/33.42 | | | | (162) all_836_0 = 0 % 225.28/33.42 | | | | % 225.28/33.42 | | | | COMBINE_EQS: (147), (162) imply: % 225.28/33.42 | | | | (163) all_1089_0 = 0 % 225.28/33.42 | | | | % 225.28/33.42 | | | | BETA: splitting (115) gives: % 225.28/33.42 | | | | % 225.28/33.42 | | | | Case 1: % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | (164) $lesseq(1, all_1089_0) % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | REDUCE: (163), (164) imply: % 225.28/33.42 | | | | | (165) $false % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | CLOSE: (165) is inconsistent. % 225.28/33.42 | | | | | % 225.28/33.42 | | | | Case 2: % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | (166) all_1089_2 = 0 % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | COMBINE_EQS: (131), (166) imply: % 225.28/33.42 | | | | | (167) all_836_3 = 0 % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | SIMP: (167) implies: % 225.28/33.42 | | | | | (168) all_836_3 = 0 % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | REDUCE: (160), (168) imply: % 225.28/33.42 | | | | | (169) $false % 225.28/33.42 | | | | | % 225.28/33.42 | | | | | CLOSE: (169) is inconsistent. % 225.28/33.42 | | | | | % 225.28/33.42 | | | | End of split % 225.28/33.42 | | | | % 225.28/33.42 | | | End of split % 225.28/33.42 | | | % 225.28/33.42 | | End of split % 225.28/33.42 | | % 225.28/33.42 | End of split % 225.28/33.42 | % 225.28/33.42 End of proof % 225.28/33.42 % SZS output end Proof for theBenchmark % 225.28/33.42 % 225.28/33.42 32811ms %------------------------------------------------------------------------------