%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP341_1 : TPTP v8.1.2. Released v8.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n003.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:48 EDT 2023 % Result : Theorem 29.40s 4.78s % Output : Proof 64.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.15 % Problem : ITP341_1 : TPTP v8.1.2. Released v8.0.0. % 0.13/0.16 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.36 % Computer : n003.cluster.edu % 0.16/0.36 % Model : x86_64 x86_64 % 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.36 % Memory : 8042.1875MB % 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.36 % CPULimit : 300 % 0.16/0.36 % WCLimit : 300 % 0.16/0.36 % DateTime : Sun Aug 27 13:50:54 EDT 2023 % 0.16/0.36 % CPUTime : % 0.22/0.64 ________ _____ % 0.22/0.64 ___ __ \_________(_)________________________________ % 0.22/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.22/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.22/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.22/0.64 % 0.22/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.22/0.64 (2023-06-19) % 0.22/0.64 % 0.22/0.64 (c) Philipp Rümmer, 2009-2023 % 0.22/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.22/0.64 Amanda Stjerna. % 0.22/0.64 Free software under BSD-3-Clause. % 0.22/0.64 % 0.22/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.22/0.64 % 0.22/0.64 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.22/0.65 Running up to 7 provers in parallel. % 0.22/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.22/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.22/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.22/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.22/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.22/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.22/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 10.41/2.21 Prover 2: Preprocessing ... % 10.41/2.23 Prover 3: Preprocessing ... % 10.41/2.24 Prover 0: Preprocessing ... % 10.41/2.24 Prover 1: Preprocessing ... % 10.84/2.27 Prover 5: Preprocessing ... % 10.84/2.27 Prover 4: Preprocessing ... % 10.84/2.27 Prover 6: Preprocessing ... % 25.67/4.27 Prover 1: Warning: ignoring some quantifiers % 25.95/4.30 Prover 3: Warning: ignoring some quantifiers % 25.95/4.33 Prover 6: Proving ... % 26.52/4.36 Prover 3: Constructing countermodel ... % 26.52/4.39 Prover 1: Constructing countermodel ... % 28.29/4.65 Prover 4: Warning: ignoring some quantifiers % 28.78/4.72 Prover 5: Proving ... % 29.40/4.78 Prover 3: proved (4115ms) % 29.40/4.78 % 29.40/4.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.40/4.78 % 29.40/4.78 Prover 6: stopped % 29.40/4.79 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.40/4.79 Prover 5: stopped % 29.40/4.80 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.40/4.80 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.98/4.85 Prover 4: Constructing countermodel ... % 29.98/4.86 Prover 0: Proving ... % 29.98/4.86 Prover 0: stopped % 29.98/4.86 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 34.54/5.50 Prover 7: Preprocessing ... % 35.01/5.54 Prover 11: Preprocessing ... % 35.41/5.57 Prover 8: Preprocessing ... % 35.41/5.64 Prover 10: Preprocessing ... % 36.31/5.70 Prover 2: Proving ... % 36.31/5.70 Prover 2: stopped % 36.31/5.72 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 38.95/6.12 Prover 13: Preprocessing ... % 42.43/6.49 Prover 8: Warning: ignoring some quantifiers % 42.43/6.55 Prover 8: Constructing countermodel ... % 44.57/6.79 Prover 10: Warning: ignoring some quantifiers % 45.13/6.87 Prover 10: Constructing countermodel ... % 45.13/6.88 Prover 7: Warning: ignoring some quantifiers % 46.01/6.99 Prover 7: Constructing countermodel ... % 47.44/7.24 Prover 11: Warning: ignoring some quantifiers % 47.44/7.35 Prover 11: Constructing countermodel ... % 49.29/7.47 Prover 13: Warning: ignoring some quantifiers % 49.95/7.56 Prover 13: Constructing countermodel ... % 62.36/9.12 Prover 7: Found proof (size 301) % 62.36/9.12 Prover 7: proved (4341ms) % 62.36/9.12 Prover 11: stopped % 62.36/9.12 Prover 13: stopped % 62.36/9.12 Prover 10: stopped % 62.36/9.12 Prover 8: stopped % 62.36/9.12 Prover 1: stopped % 62.36/9.13 Prover 4: stopped % 62.36/9.13 % 62.36/9.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.36/9.13 % 62.82/9.28 % SZS output start Proof for theBenchmark % 62.82/9.29 Assumptions after simplification: % 62.82/9.29 --------------------------------- % 62.82/9.29 % 62.82/9.30 (axiom10) % 63.18/9.32 A_n_vec_n_vec$(p$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : ? [v1: % 63.18/9.32 A_n_vec_n_vec$] : ? [v2: A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : % 63.18/9.32 (matrix_inv$(p$) = v0 & matrix_matrix_mult$(v1, a$) = v2 & % 63.18/9.32 matrix_matrix_mult$(v0, v3) = v2 & matrix_matrix_mult$(v0, p$) = v1 & % 63.18/9.32 matrix_matrix_mult$(p$, a$) = v3 & A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & % 63.18/9.32 A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0)) % 63.18/9.32 % 63.18/9.32 (axiom11) % 63.18/9.32 A$(one$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & % 63.18/9.32 matrix_matrix_mult$(v0, a$) = a$ & A_n_vec_n_vec$(v0)) % 63.18/9.32 % 63.18/9.32 (axiom12) % 63.18/9.33 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.33 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.18/9.33 (matrix_matrix_mult$(v2, v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.18/9.33 A_n_vec_n_vec$(v1) | ? [v3: A_n_vec_n_vec$] : ? [v4: A_n_vec_n_vec$] : % 63.18/9.33 ((v4 = v2 & matrix_inv$(v1) = v2) | ( ~ (v3 = v0) & % 63.18/9.33 matrix_matrix_mult$(v1, v2) = v3 & A_n_vec_n_vec$(v3)))) & ! [v1: % 63.18/9.33 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, % 63.18/9.33 v2) = v0) | ~ A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v3: % 63.18/9.33 A_n_vec_n_vec$] : ? [v4: A_n_vec_n_vec$] : ((v4 = v2 & matrix_inv$(v1) % 63.18/9.33 = v2) | ( ~ (v3 = v0) & matrix_matrix_mult$(v2, v1) = v3 & % 63.18/9.33 A_n_vec_n_vec$(v3))))) % 63.18/9.33 % 63.18/9.33 (axiom122) % 63.18/9.33 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.33 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A$] : ! [v2: A$] : ! [v3: % 63.18/9.33 N$] : ! [v4: A_n_vec_n_vec$] : ( ~ (times$(v2, v1) = one$) | ~ % 63.18/9.33 (mult_row$(v0, v3, v1) = v4) | ~ A$(v2) | ~ A$(v1) | ~ N$(v3) | % 63.18/9.33 fun_app$(invertible$, v4) | ? [v5: A$] : ( ~ (v5 = one$) & times$(v1, v2) % 63.18/9.33 = v5 & A$(v5))) & ! [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: % 63.18/9.33 A_n_vec_n_vec$] : ( ~ (times$(v1, v2) = one$) | ~ (mult_row$(v0, v3, v1) % 63.18/9.33 = v4) | ~ A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, v4) | % 63.18/9.33 ? [v5: A$] : ( ~ (v5 = one$) & times$(v2, v1) = v5 & A$(v5)))) % 63.18/9.33 % 63.18/9.33 (axiom123) % 63.18/9.33 A$(zero$) & A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: % 63.18/9.33 A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A$] : ! % 63.18/9.33 [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = zero$ | ~ (mult_row$(v0, v2, v1) % 63.18/9.33 = v3) | ~ A$(v1) | ~ N$(v2) | fun_app$(invertible$, v3))) % 63.18/9.33 % 63.18/9.33 (axiom13) % 63.18/9.34 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.34 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : % 63.18/9.34 (v3 = v0 | ~ (matrix_matrix_mult$(v2, v1) = v3) | ~ A_n_vec_n_vec$(v2) | % 63.18/9.34 ~ A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : ( ~ (v4 = v0) & % 63.18/9.34 matrix_matrix_mult$(v1, v2) = v4 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.18/9.34 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v3 % 63.18/9.34 = v0 | ~ (matrix_matrix_mult$(v1, v2) = v3) | ~ A_n_vec_n_vec$(v2) | ~ % 63.18/9.34 A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : ( ~ (v4 = v0) & % 63.18/9.34 matrix_matrix_mult$(v2, v1) = v4 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.18/9.34 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v2, % 63.18/9.34 v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | % 63.18/9.34 matrix_matrix_mult$(v1, v2) = v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.34 A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, v2) = v0) | ~ % 63.18/9.34 A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | matrix_matrix_mult$(v2, v1) = % 63.18/9.34 v0)) % 63.18/9.34 % 63.18/9.34 (axiom14) % 63.18/9.34 A_n_vec_n_vec$(p$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.34 (gauss_Jordan$(a$) = v0 & matrix_matrix_mult$(p$, a$) = v0 & % 63.18/9.34 A_n_vec_n_vec$(v0)) % 63.18/9.34 % 63.18/9.34 (axiom15) % 63.18/9.34 A$(one$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : (gauss_Jordan$(a$) = % 63.18/9.34 v0 & mat$(one$) = v0 & A_n_vec_n_vec$(v0)) % 63.18/9.34 % 63.18/9.34 (axiom159) % 63.18/9.34 A_n_vec$(zero$c) & A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & % 63.18/9.34 A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec$] : ! [v3: % 63.18/9.34 A_n_vec_n_vec$] : (v2 = zero$c | ~ (matrix_vector_mult$(v1, v2) = zero$c) % 63.18/9.34 | ~ (matrix_matrix_mult$(v3, v1) = v0) | ~ A_n_vec$(v2) | ~ % 63.18/9.34 A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1)) & ? [v1: A_n_vec_n_vec$] : ( % 63.18/9.34 ~ A_n_vec_n_vec$(v1) | ? [v2: A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : % 63.18/9.34 ? [v4: A_n_vec$] : ? [v5: A_n_vec$] : (A_n_vec$(v4) & A_n_vec_n_vec$(v2) % 63.18/9.34 & ((v5 = zero$c & ~ (v4 = zero$c) & matrix_vector_mult$(v1, v4) = % 63.18/9.34 zero$c) | (v3 = v0 & matrix_matrix_mult$(v2, v1) = v0))))) % 63.18/9.34 % 63.18/9.34 (axiom16) % 63.18/9.34 A_n_vec_n_vec$(a$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: % 63.18/9.34 A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : (gauss_Jordan$(a$) = v0 & % 63.18/9.34 matrix_matrix_mult$(v1, a$) = v0 & A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0) & % 63.18/9.34 fun_app$(invertible$, v1)) % 63.18/9.34 % 63.18/9.34 (axiom179) % 63.18/9.34 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.34 ! [v1: A_n_vec$] : ! [v2: A_n_vec$] : (v2 = v1 | ~ % 63.18/9.34 (matrix_vector_mult$(v0, v1) = v2) | ~ A_n_vec$(v1))) % 63.18/9.34 % 63.18/9.34 (axiom18) % 63.18/9.34 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.34 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.34 A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, v2) = v0) | ~ % 63.18/9.34 A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1)) & % 63.18/9.34 ! [v1: A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ~ fun_app$(invertible$, % 63.18/9.34 v1) | ? [v2: A_n_vec_n_vec$] : (matrix_matrix_mult$(v1, v2) = v0 & % 63.18/9.34 A_n_vec_n_vec$(v2)))) % 63.18/9.34 % 63.18/9.34 (axiom19) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.35 A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v2, v1) = v0) | ~ % 63.18/9.35 A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1) | % 63.18/9.35 ? [v3: A_n_vec_n_vec$] : ( ~ (v3 = v0) & matrix_matrix_mult$(v1, v2) = v3 % 63.18/9.35 & A_n_vec_n_vec$(v3))) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.35 A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, v2) = v0) | ~ % 63.18/9.35 A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1) | % 63.18/9.35 ? [v3: A_n_vec_n_vec$] : ( ~ (v3 = v0) & matrix_matrix_mult$(v2, v1) = v3 % 63.18/9.35 & A_n_vec_n_vec$(v3))) & ! [v1: A_n_vec_n_vec$] : ( ~ % 63.18/9.35 A_n_vec_n_vec$(v1) | ~ fun_app$(invertible$, v1) | ? [v2: % 63.18/9.35 A_n_vec_n_vec$] : (matrix_matrix_mult$(v2, v1) = v0 & % 63.18/9.35 matrix_matrix_mult$(v1, v2) = v0 & A_n_vec_n_vec$(v2)))) % 63.18/9.35 % 63.18/9.35 (axiom20) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.35 A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v2, v1) = v0) | ~ % 63.18/9.35 A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1)) & % 63.18/9.35 ! [v1: A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ~ fun_app$(invertible$, % 63.18/9.35 v1) | ? [v2: A_n_vec_n_vec$] : (matrix_matrix_mult$(v2, v1) = v0 & % 63.18/9.35 A_n_vec_n_vec$(v2)))) % 63.18/9.35 % 63.18/9.35 (axiom24) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.35 A_n_vec_n_vec$] : ( ~ (matrix_inv$(v1) = v2) | ~ A_n_vec_n_vec$(v1) | ~ % 63.18/9.35 fun_app$(invertible$, v1) | matrix_matrix_mult$(v1, v2) = v0)) % 63.18/9.35 % 63.18/9.35 (axiom25) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.18/9.35 A_n_vec_n_vec$] : ( ~ (matrix_inv$(v1) = v2) | ~ A_n_vec_n_vec$(v1) | ~ % 63.18/9.35 fun_app$(invertible$, v1) | matrix_matrix_mult$(v2, v1) = v0)) % 63.18/9.35 % 63.18/9.35 (axiom28) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & fun_app$(invertible$, v0)) % 63.18/9.35 % 63.18/9.35 (axiom31) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(orthogonal_matrix$) & ? [v0: % 63.18/9.35 A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.35 fun_app$(orthogonal_matrix$, v0)) % 63.18/9.35 % 63.18/9.35 (axiom32) % 63.18/9.35 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.35 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.18/9.35 A$] : ! [v4: A_n_vec_n_vec$] : (v2 = v1 | ~ (column_add$(v0, v1, v2, v3) % 63.18/9.35 = v4) | ~ A$(v3) | ~ N$(v2) | ~ N$(v1) | fun_app$(invertible$, v4))) % 63.18/9.35 % 63.18/9.35 (axiom33) % 63.18/9.35 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.35 ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A$] : ! [v5: % 63.18/9.35 A_n_vec_n_vec$] : ! [v6: A_n_vec_n_vec$] : ( ~ (column_add$(v0, v2, v3, % 63.18/9.35 v4) = v5) | ~ (matrix_matrix_mult$(v1, v5) = v6) | ~ A$(v4) | ~ % 63.18/9.35 N$(v3) | ~ N$(v2) | ~ A_n_vec_n_vec$(v1) | (column_add$(v1, v2, v3, v4) % 63.18/9.35 = v6 & A_n_vec_n_vec$(v6))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! % 63.18/9.35 [v3: N$] : ! [v4: A$] : ! [v5: A_n_vec_n_vec$] : ( ~ (column_add$(v1, v2, % 63.18/9.35 v3, v4) = v5) | ~ A$(v4) | ~ N$(v3) | ~ N$(v2) | ~ % 63.18/9.35 A_n_vec_n_vec$(v1) | ? [v6: A_n_vec_n_vec$] : (column_add$(v0, v2, v3, % 63.18/9.35 v4) = v6 & matrix_matrix_mult$(v1, v6) = v5 & A_n_vec_n_vec$(v6) & % 63.18/9.35 A_n_vec_n_vec$(v5)))) % 63.18/9.35 % 63.18/9.35 (axiom35) % 63.18/9.35 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.35 ! [v1: A_n_vec$] : ! [v2: A_n_vec$] : (v2 = v1 | ~ % 63.18/9.35 (vector_matrix_mult$a(v1, v0) = v2) | ~ A_n_vec$(v1))) % 63.18/9.35 % 63.18/9.35 (axiom36) % 63.18/9.36 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.36 ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] % 63.18/9.36 : ! [v5: A_n_vec_n_vec$] : ( ~ (mult_column$(v0, v2, v3) = v4) | ~ % 63.18/9.36 (matrix_matrix_mult$(v1, v4) = v5) | ~ A$(v3) | ~ N$(v2) | ~ % 63.18/9.36 A_n_vec_n_vec$(v1) | (mult_column$(v1, v2, v3) = v5 & A_n_vec_n_vec$(v5))) % 63.18/9.36 & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: A$] : ! [v4: % 63.18/9.36 A_n_vec_n_vec$] : ( ~ (mult_column$(v1, v2, v3) = v4) | ~ A$(v3) | ~ % 63.18/9.36 N$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v5: A_n_vec_n_vec$] : % 63.18/9.36 (mult_column$(v0, v2, v3) = v5 & matrix_matrix_mult$(v1, v5) = v4 & % 63.18/9.36 A_n_vec_n_vec$(v5) & A_n_vec_n_vec$(v4)))) % 63.18/9.36 % 63.18/9.36 (axiom37) % 63.18/9.36 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.36 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.18/9.36 A_n_vec_n_vec$] : ( ~ (interchange_columns$(v0, v1, v2) = v3) | ~ N$(v2) % 63.18/9.36 | ~ N$(v1) | fun_app$(invertible$, v3))) % 63.18/9.36 % 63.18/9.36 (axiom38) % 63.18/9.36 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.36 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : % 63.18/9.36 ( ~ (transpose$(v1) = v2) | ~ (matrix_matrix_mult$(v3, v1) = v0) | ~ % 63.18/9.36 A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.18/9.36 (matrix_matrix_mult$(v2, v4) = v0 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.18/9.36 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : ( ~ % 63.18/9.36 (transpose$(v1) = v2) | ~ (matrix_matrix_mult$(v2, v3) = v0) | ~ % 63.18/9.36 A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.18/9.36 (matrix_matrix_mult$(v4, v1) = v0 & A_n_vec_n_vec$(v4)))) % 63.18/9.36 % 63.18/9.36 (axiom46) % 63.18/9.36 A$(one$) & A_n_vec_n_vec_bool_fun$(orthogonal_matrix$) & ? [v0: % 63.18/9.36 A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: % 63.18/9.36 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.18/9.36 A_n_vec_n_vec$(v1) | ~ fun_app$(orthogonal_matrix$, v1) | % 63.18/9.36 (matrix_matrix_mult$(v2, v1) = v0 & matrix_matrix_mult$(v1, v2) = v0)) & % 63.18/9.36 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) % 63.18/9.36 | ~ A_n_vec_n_vec$(v1) | fun_app$(orthogonal_matrix$, v1) | ? [v3: % 63.18/9.36 A_n_vec_n_vec$] : ? [v4: A_n_vec_n_vec$] : (( ~ (v4 = v0) & % 63.18/9.36 matrix_matrix_mult$(v1, v2) = v4 & A_n_vec_n_vec$(v4)) | ( ~ (v3 = v0) % 63.18/9.36 & matrix_matrix_mult$(v2, v1) = v3 & A_n_vec_n_vec$(v3))))) % 63.18/9.36 % 63.18/9.36 (axiom47) % 63.18/9.36 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.36 ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] % 63.18/9.36 : ! [v5: A_n_vec_n_vec$] : ( ~ (interchange_columns$(v0, v2, v3) = v4) | ~ % 63.18/9.36 (matrix_matrix_mult$(v1, v4) = v5) | ~ N$(v3) | ~ N$(v2) | ~ % 63.18/9.36 A_n_vec_n_vec$(v1) | (interchange_columns$(v1, v2, v3) = v5 & % 63.18/9.36 A_n_vec_n_vec$(v5))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: % 63.18/9.36 N$] : ! [v4: A_n_vec_n_vec$] : ( ~ (interchange_columns$(v1, v2, v3) = % 63.18/9.36 v4) | ~ N$(v3) | ~ N$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v5: % 63.18/9.36 A_n_vec_n_vec$] : (interchange_columns$(v0, v2, v3) = v5 & % 63.18/9.36 matrix_matrix_mult$(v1, v5) = v4 & A_n_vec_n_vec$(v5) & % 63.18/9.36 A_n_vec_n_vec$(v4)))) % 63.18/9.36 % 63.18/9.36 (axiom48) % 63.18/9.36 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.36 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : % 63.18/9.36 ( ~ (transpose$(v1) = v2) | ~ (matrix_matrix_mult$(v3, v2) = v0) | ~ % 63.18/9.36 A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.18/9.36 (matrix_matrix_mult$(v1, v4) = v0 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.18/9.36 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : ( ~ % 63.18/9.36 (transpose$(v1) = v2) | ~ (matrix_matrix_mult$(v1, v3) = v0) | ~ % 63.18/9.36 A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.18/9.36 (matrix_matrix_mult$(v4, v2) = v0 & A_n_vec_n_vec$(v4)))) % 63.18/9.36 % 63.18/9.36 (axiom5) % 63.18/9.36 A$(one$) & A_n_vec_n_vec$(p$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.36 ? [v1: A_n_vec_n_vec$] : ? [v2: A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : % 63.18/9.36 (mat$(one$) = v0 & matrix_inv$(p$) = v2 & matrix_matrix_mult$(v3, a$) = v1 & % 63.18/9.36 matrix_matrix_mult$(v2, p$) = v3 & matrix_matrix_mult$(v0, a$) = v1 & % 63.18/9.36 A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & % 63.18/9.36 A_n_vec_n_vec$(v0)) % 63.18/9.36 % 63.18/9.36 (axiom56) % 63.18/9.37 A$(zero$) & A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: % 63.18/9.37 A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A$] : ! % 63.18/9.37 [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = zero$ | ~ (mult_column$(v0, v2, % 63.18/9.37 v1) = v3) | ~ A$(v1) | ~ N$(v2) | fun_app$(invertible$, v3))) % 63.18/9.37 % 63.18/9.37 (axiom57) % 63.18/9.37 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.37 ! [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] % 63.18/9.37 : ! [v5: A_n_vec_n_vec$] : ( ~ (mult_row$(v0, v1, v2) = v4) | ~ % 63.18/9.37 (matrix_matrix_mult$(v4, v3) = v5) | ~ A$(v2) | ~ N$(v1) | ~ % 63.18/9.37 A_n_vec_n_vec$(v3) | (mult_row$(v3, v1, v2) = v5 & A_n_vec_n_vec$(v5))) & % 63.18/9.37 ! [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] % 63.18/9.37 : ( ~ (mult_row$(v3, v1, v2) = v4) | ~ A$(v2) | ~ N$(v1) | ~ % 63.18/9.37 A_n_vec_n_vec$(v3) | ? [v5: A_n_vec_n_vec$] : (mult_row$(v0, v1, v2) = v5 % 63.18/9.37 & matrix_matrix_mult$(v5, v3) = v4 & A_n_vec_n_vec$(v5) & % 63.18/9.37 A_n_vec_n_vec$(v4)))) % 63.18/9.37 % 63.18/9.37 (axiom58) % 63.18/9.37 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.37 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: A$] : ! [v2: A$] : ! [v3: % 63.18/9.37 N$] : ! [v4: A_n_vec_n_vec$] : ( ~ (times$(v2, v1) = one$) | ~ % 63.18/9.37 (mult_column$(v0, v3, v1) = v4) | ~ A$(v2) | ~ A$(v1) | ~ N$(v3) | % 63.18/9.37 fun_app$(invertible$, v4) | ? [v5: A$] : ( ~ (v5 = one$) & times$(v1, v2) % 63.18/9.37 = v5 & A$(v5))) & ! [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: % 63.18/9.37 A_n_vec_n_vec$] : ( ~ (times$(v1, v2) = one$) | ~ (mult_column$(v0, v3, % 63.18/9.37 v1) = v4) | ~ A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, % 63.18/9.37 v4) | ? [v5: A$] : ( ~ (v5 = one$) & times$(v2, v1) = v5 & A$(v5)))) % 63.18/9.37 % 63.18/9.37 (axiom6) % 63.18/9.37 A$(one$) & A_n_vec_n_vec$(p$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.37 ? [v1: A_n_vec_n_vec$] : ? [v2: A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : % 63.18/9.37 (mat$(one$) = v3 & matrix_inv$(p$) = v0 & matrix_matrix_mult$(v0, v3) = v2 & % 63.18/9.37 matrix_matrix_mult$(v0, v1) = v2 & matrix_matrix_mult$(p$, a$) = v1 & % 63.18/9.37 A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & % 63.18/9.37 A_n_vec_n_vec$(v0)) % 63.18/9.37 % 63.18/9.37 (axiom60) % 63.18/9.37 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.37 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.18/9.37 N_a_n_vec_n_vec_fun$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.18/9.37 (interchange_rows$(v0, v1) = v3) | ~ (fun_app$c(v3, v2) = v4) | ~ N$(v2) % 63.18/9.37 | ~ N$(v1) | fun_app$(invertible$, v4))) % 63.18/9.37 % 63.18/9.37 (axiom61) % 63.18/9.37 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.37 ! [v1: N$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ! [v4: % 63.18/9.37 N_a_n_vec_n_vec_fun$] : ! [v5: A_n_vec_n_vec$] : ! [v6: A_n_vec_n_vec$] % 63.18/9.37 : ( ~ (interchange_rows$(v0, v1) = v4) | ~ (fun_app$c(v4, v2) = v5) | ~ % 63.18/9.37 (matrix_matrix_mult$(v5, v3) = v6) | ~ N$(v2) | ~ N$(v1) | ~ % 63.18/9.37 A_n_vec_n_vec$(v3) | ? [v7: N_a_n_vec_n_vec_fun$] : % 63.18/9.37 (interchange_rows$(v3, v1) = v7 & fun_app$c(v7, v2) = v6 & % 63.18/9.37 N_a_n_vec_n_vec_fun$(v7) & A_n_vec_n_vec$(v6))) & ! [v1: N$] : ! [v2: % 63.18/9.37 N$] : ! [v3: A_n_vec_n_vec$] : ! [v4: N_a_n_vec_n_vec_fun$] : ! [v5: % 63.18/9.37 A_n_vec_n_vec$] : ( ~ (interchange_rows$(v3, v1) = v4) | ~ (fun_app$c(v4, % 63.18/9.37 v2) = v5) | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v3) | ? [v6: % 63.18/9.37 N_a_n_vec_n_vec_fun$] : ? [v7: A_n_vec_n_vec$] : (interchange_rows$(v0, % 63.18/9.37 v1) = v6 & fun_app$c(v6, v2) = v7 & matrix_matrix_mult$(v7, v3) = v5 & % 63.18/9.37 N_a_n_vec_n_vec_fun$(v6) & A_n_vec_n_vec$(v7) & A_n_vec_n_vec$(v5)))) % 63.18/9.37 % 63.18/9.37 (axiom62) % 63.18/9.38 A$(one$) & A_n_vec_n_vec_bool_fun$(invertible$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.38 (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.18/9.38 A$] : ! [v4: A_n_vec_n_vec$] : (v2 = v1 | ~ (row_add$(v0, v1, v2, v3) = % 63.18/9.38 v4) | ~ A$(v3) | ~ N$(v2) | ~ N$(v1) | fun_app$(invertible$, v4))) % 63.18/9.38 % 63.18/9.38 (axiom63) % 63.18/9.38 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.38 ! [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : ! [v5: % 63.18/9.38 A_n_vec_n_vec$] : ! [v6: A_n_vec_n_vec$] : ( ~ (row_add$(v0, v1, v2, v3) % 63.18/9.38 = v5) | ~ (matrix_matrix_mult$(v5, v4) = v6) | ~ A$(v3) | ~ N$(v2) | % 63.18/9.38 ~ N$(v1) | ~ A_n_vec_n_vec$(v4) | (row_add$(v4, v1, v2, v3) = v6 & % 63.18/9.38 A_n_vec_n_vec$(v6))) & ! [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: % 63.18/9.38 A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ (row_add$(v4, v1, v2, v3) % 63.18/9.38 = v5) | ~ A$(v3) | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v4) | ? % 63.18/9.38 [v6: A_n_vec_n_vec$] : (row_add$(v0, v1, v2, v3) = v6 & % 63.18/9.38 matrix_matrix_mult$(v6, v4) = v5 & A_n_vec_n_vec$(v6) & % 63.18/9.38 A_n_vec_n_vec$(v5)))) % 63.18/9.38 % 63.18/9.38 (axiom7) % 63.18/9.38 A$(one$) & A_n_vec_n_vec$(p$) & A_n_vec_n_vec$(a$) & ? [v0: A_n_vec_n_vec$] : % 63.18/9.38 ? [v1: A_n_vec_n_vec$] : (mat$(one$) = v1 & matrix_inv$(p$) = v0 & % 63.18/9.38 matrix_matrix_mult$(v0, v1) = a$ & A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0)) % 63.18/9.38 % 63.18/9.38 (axiom8) % 63.18/9.38 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.38 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v2 = v1 | ~ % 63.18/9.38 (matrix_matrix_mult$(v0, v1) = v2) | ~ A_n_vec_n_vec$(v1))) % 63.18/9.38 % 63.18/9.38 (axiom9) % 63.18/9.38 A$(one$) & ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.18/9.38 ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v2 = v1 | ~ % 63.18/9.38 (matrix_matrix_mult$(v1, v0) = v2) | ~ A_n_vec_n_vec$(v1))) % 63.18/9.38 % 63.18/9.38 (conjecture3) % 63.18/9.38 A$(one$) & A_n_vec_n_vec$(p$) & ? [v0: A_n_vec_n_vec$] : ? [v1: % 63.18/9.38 A_n_vec_n_vec$] : ? [v2: A_n_vec_n_vec$] : ( ~ (v2 = v0) & mat$(one$) = v1 % 63.18/9.38 & matrix_inv$(p$) = v0 & matrix_matrix_mult$(v0, v1) = v2 & % 63.18/9.38 A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0)) % 63.18/9.38 % 63.18/9.38 (function-axioms) % 63.61/9.40 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] % 63.61/9.40 : ! [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (row_add$(v5, v4, v3, % 63.61/9.40 v2) = v1) | ~ (row_add$(v5, v4, v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] : ! % 63.61/9.40 [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (column_add$(v5, v4, v3, % 63.61/9.40 v2) = v1) | ~ (column_add$(v5, v4, v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] : ! % 63.61/9.40 [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (mult_row$(v4, v3, v2) = v1) | ~ % 63.61/9.40 (mult_row$(v4, v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 % 63.61/9.40 = v0 | ~ (interchange_columns$(v4, v3, v2) = v1) | ~ % 63.61/9.40 (interchange_columns$(v4, v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 % 63.61/9.40 = v0 | ~ (mult_column$(v4, v3, v2) = v1) | ~ (mult_column$(v4, v3, v2) = % 63.61/9.40 v0)) & ! [v0: A_n_vec_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec_n_vec$] : ! % 63.61/9.40 [v2: A_n_vec_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.40 (plus$i(v3, v2) = v1) | ~ (plus$i(v3, v2) = v0)) & ! [v0: A$] : ! [v1: % 63.61/9.40 A$] : ! [v2: A$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = % 63.61/9.40 v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 63.61/9.40 A$] : ! [v3: A$] : (v1 = v0 | ~ (plus$h(v3, v2) = v1) | ~ (plus$h(v3, v2) % 63.61/9.40 = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (plus$g(v3, v2) = % 63.61/9.40 v1) | ~ (plus$g(v3, v2) = v0)) & ! [v0: A_n_vec_set_set$] : ! [v1: % 63.61/9.40 A_n_vec_set_set$] : ! [v2: A_n_vec_set_set$] : ! [v3: A_n_vec_set_set$] : % 63.61/9.40 (v1 = v0 | ~ (plus$f(v3, v2) = v1) | ~ (plus$f(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec$] : (v1 % 63.61/9.40 = v0 | ~ (plus$d(v3, v2) = v1) | ~ (plus$d(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_set$] : ! [v3: % 63.61/9.40 A_n_vec_set$] : (v1 = v0 | ~ (plus$e(v3, v2) = v1) | ~ (plus$e(v3, v2) = % 63.61/9.40 v0)) & ! [v0: A_n_vec_n_vec_set$] : ! [v1: A_n_vec_n_vec_set$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec_set$] : ! [v3: A_n_vec_n_vec_set$] : (v1 = v0 | ~ % 63.61/9.40 (plus$b(v3, v2) = v1) | ~ (plus$b(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec_set_set$] : ! [v1: A_n_vec_n_vec_set_set$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec_set_set$] : ! [v3: A_n_vec_n_vec_set_set$] : (v1 = v0 | ~ % 63.61/9.40 (plus$c(v3, v2) = v1) | ~ (plus$c(v3, v2) = v0)) & ! [v0: A_set$] : ! % 63.61/9.40 [v1: A_set$] : ! [v2: A_set$] : ! [v3: A_set$] : (v1 = v0 | ~ (plus$(v3, % 63.61/9.40 v2) = v1) | ~ (plus$(v3, v2) = v0)) & ! [v0: A_set_set$] : ! [v1: % 63.61/9.40 A_set_set$] : ! [v2: A_set_set$] : ! [v3: A_set_set$] : (v1 = v0 | ~ % 63.61/9.40 (plus$a(v3, v2) = v1) | ~ (plus$a(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! % 63.61/9.40 [v1: A_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: N$] : (v1 = v0 | ~ % 63.61/9.40 (column$(v3, v2) = v1) | ~ (column$(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! % 63.61/9.40 [v3: A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_vector_mult$a(v3, v2) = v1) % 63.61/9.40 | ~ (matrix_vector_mult$a(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec$] : ! [v2: A$] : ! [v3: N$] : (v1 = v0 | ~ (axis$a(v3, v2) = v1) % 63.61/9.40 | ~ (axis$a(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec$] : ! [v2: A_n_vec$] : ! [v3: N$] : (v1 = v0 | ~ (axis$(v3, % 63.61/9.40 v2) = v1) | ~ (axis$(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.40 (matrix_vector_mult$(v3, v2) = v1) | ~ (matrix_vector_mult$(v3, v2) = v0)) % 63.61/9.40 & ! [v0: Num$] : ! [v1: Num$] : ! [v2: Num$] : ! [v3: Num$] : (v1 = v0 | % 63.61/9.40 ~ (times$g(v3, v2) = v1) | ~ (times$g(v3, v2) = v0)) & ! [v0: Num_set$] : % 63.61/9.40 ! [v1: Num_set$] : ! [v2: Num_set$] : ! [v3: Num_set$] : (v1 = v0 | ~ % 63.61/9.40 (times$h(v3, v2) = v1) | ~ (times$h(v3, v2) = v0)) & ! [v0: A_set_set$] : % 63.61/9.40 ! [v1: A_set_set$] : ! [v2: A_set_set$] : ! [v3: A_set_set$] : (v1 = v0 | ~ % 63.61/9.40 (times$f(v3, v2) = v1) | ~ (times$f(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec_set$] : ! [v1: A_n_vec_n_vec_set$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec_set$] : ! [v3: A_n_vec_n_vec_set$] : (v1 = v0 | ~ % 63.61/9.40 (times$e(v3, v2) = v1) | ~ (times$e(v3, v2) = v0)) & ! [v0: A_n_vec_set$] % 63.61/9.40 : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_set$] : (v1 % 63.61/9.40 = v0 | ~ (times$d(v3, v2) = v1) | ~ (times$d(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_set$] : ! [v1: A_set$] : ! [v2: A_set$] : ! [v3: A_set$] : (v1 = v0 | % 63.61/9.40 ~ (times$c(v3, v2) = v1) | ~ (times$c(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! % 63.61/9.40 [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (times$b(v3, v2) = v1) | ~ (times$b(v3, % 63.61/9.40 v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec$] : % 63.61/9.40 ! [v3: A_n_vec$] : (v1 = v0 | ~ (times$a(v3, v2) = v1) | ~ (times$a(v3, v2) % 63.61/9.40 = v0)) & ! [v0: N_a_n_vec_n_vec_fun$] : ! [v1: N_a_n_vec_n_vec_fun$] : % 63.61/9.40 ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (interchange_rows$(v3, % 63.61/9.40 v2) = v1) | ~ (interchange_rows$(v3, v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: % 63.61/9.40 N_a_n_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | ~ % 63.61/9.40 (fun_app$c(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A$] : ! % 63.61/9.40 [v3: A$] : (v1 = v0 | ~ (times$(v3, v2) = v1) | ~ (times$(v3, v2) = v0)) & % 63.61/9.40 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: Nat$] : ! [v3: % 63.61/9.40 A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan_upt_k$(v3, v2) = v1) | ~ % 63.61/9.40 (gauss_Jordan_upt_k$(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec_n_vec$] : ! % 63.61/9.40 [v1: A_n_vec_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec_n_vec$] : ! [v3: % 63.61/9.40 A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$a(v3, v2) = v1) | % 63.61/9.40 ~ (matrix_matrix_mult$a(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec$] : (v1 = v0 | ~ % 63.61/9.40 (vector_matrix_mult$a(v3, v2) = v1) | ~ (vector_matrix_mult$a(v3, v2) = % 63.61/9.40 v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.40 (vector_matrix_mult$(v3, v2) = v1) | ~ (vector_matrix_mult$(v3, v2) = v0)) % 63.61/9.40 & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] % 63.61/9.40 : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$(v3, v2) = v1) | % 63.61/9.40 ~ (matrix_matrix_mult$(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 63.61/9.40 Num$] : (v1 = v0 | ~ (numeral$b(v2) = v1) | ~ (numeral$b(v2) = v0)) & ! % 63.61/9.40 [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: Num$] : (v1 = v0 | ~ % 63.61/9.40 (numeral$a(v2) = v1) | ~ (numeral$a(v2) = v0)) & ! [v0: A_n_vec$] : ! % 63.61/9.40 [v1: A_n_vec$] : ! [v2: Num$] : (v1 = v0 | ~ (numeral$(v2) = v1) | ~ % 63.61/9.40 (numeral$(v2) = v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : % 63.61/9.40 (v1 = v0 | ~ (divide$(v2) = v1) | ~ (divide$(v2) = v0)) & ! [v0: A$] : ! % 63.61/9.40 [v1: A$] : ! [v2: A$] : (v1 = v0 | ~ (dbl_inc$b(v2) = v1) | ~ % 63.61/9.40 (dbl_inc$b(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: % 63.61/9.40 A_n_vec$] : (v1 = v0 | ~ (dbl_inc$a(v2) = v1) | ~ (dbl_inc$a(v2) = v0)) & % 63.61/9.40 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : % 63.61/9.40 (v1 = v0 | ~ (dbl_inc$(v2) = v1) | ~ (dbl_inc$(v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec$] : (v1 = v0 | % 63.61/9.40 ~ (rowvector$(v2) = v1) | ~ (rowvector$(v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec$] : (v1 = v0 | % 63.61/9.40 ~ (columnvector$(v2) = v1) | ~ (columnvector$(v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec_n_vec$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ (transpose$a(v2) = v1) | ~ % 63.61/9.40 (transpose$a(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] % 63.61/9.40 : ! [v2: A_n_vec$] : (v1 = v0 | ~ (vec$a(v2) = v1) | ~ (vec$a(v2) = v0)) & % 63.61/9.40 ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A$] : (v1 = v0 | ~ (vec$(v2) = % 63.61/9.40 v1) | ~ (vec$(v2) = v0)) & ! [v0: A_n_vec_set$] : ! [v1: A_n_vec_set$] % 63.61/9.40 : ! [v2: A_n_vec_bool_fun$] : (v1 = v0 | ~ (collect$b(v2) = v1) | ~ % 63.61/9.40 (collect$b(v2) = v0)) & ! [v0: A_n_vec_n_vec_set$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec_set$] : ! [v2: A_n_vec_n_vec_bool_fun$] : (v1 = v0 | ~ % 63.61/9.40 (collect$a(v2) = v1) | ~ (collect$a(v2) = v0)) & ! [v0: A_set$] : ! [v1: % 63.61/9.40 A_set$] : ! [v2: A_bool_fun$] : (v1 = v0 | ~ (collect$(v2) = v1) | ~ % 63.61/9.40 (collect$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : % 63.61/9.40 ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (transpose$(v2) = v1) | ~ % 63.61/9.40 (transpose$(v2) = v0)) & ! [v0: A_n_vec_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec_n_vec$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (mat$a(v2) = v1) | % 63.61/9.40 ~ (mat$a(v2) = v0)) & ! [v0: A_n_vec_n_vec_bool_fun$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec_bool_fun$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.40 (similar_matrices$(v2) = v1) | ~ (similar_matrices$(v2) = v0)) & ! [v0: % 63.61/9.40 A_n_vec_n_vec_bool_fun$] : ! [v1: A_n_vec_n_vec_bool_fun$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec$] : (v1 = v0 | ~ (equivalent_matrices$(v2) = v1) | ~ % 63.61/9.40 (equivalent_matrices$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan$(v2) % 63.61/9.40 = v1) | ~ (gauss_Jordan$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec$] : ! [v2: A$] : (v1 = v0 | ~ (mat$(v2) = v1) | ~ (mat$(v2) % 63.61/9.40 = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.40 A_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_inv$(v2) = v1) | ~ (matrix_inv$(v2) % 63.61/9.40 = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A_set$] : % 63.61/9.40 (v1 = v0 | ~ (uu$(v2) = v1) | ~ (uu$(v2) = v0)) & ! [v0: A_n_vec_bool_fun$] % 63.61/9.40 : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (uub$(v2) % 63.61/9.40 = v1) | ~ (uub$(v2) = v0)) & ! [v0: A_n_vec_n_vec_bool_fun$] : ! [v1: % 63.61/9.40 A_n_vec_n_vec_bool_fun$] : ! [v2: A_n_vec_n_vec_set$] : (v1 = v0 | ~ % 63.61/9.40 (uua$(v2) = v1) | ~ (uua$(v2) = v0)) % 63.61/9.40 % 63.61/9.40 Further assumptions not needed in the proof: % 63.61/9.40 -------------------------------------------- % 63.61/9.40 axiom0, axiom1, axiom100, axiom101, axiom102, axiom103, axiom104, axiom105, % 63.61/9.40 axiom106, axiom107, axiom108, axiom109, axiom110, axiom111, axiom112, axiom113, % 63.61/9.40 axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, axiom120, axiom121, % 63.61/9.40 axiom124, axiom125, axiom126, axiom127, axiom128, axiom129, axiom130, axiom131, % 63.61/9.40 axiom132, axiom133, axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, % 63.61/9.40 axiom140, axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, % 63.61/9.40 axiom148, axiom149, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 63.61/9.40 axiom156, axiom157, axiom158, axiom160, axiom161, axiom162, axiom163, axiom164, % 63.61/9.40 axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, % 63.61/9.40 axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom180, % 63.61/9.40 axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, axiom187, axiom188, % 63.61/9.40 axiom189, axiom190, axiom191, axiom192, axiom193, axiom194, axiom195, axiom196, % 63.61/9.40 axiom197, axiom198, axiom199, axiom2, axiom200, axiom201, axiom202, axiom203, % 63.61/9.40 axiom204, axiom205, axiom206, axiom207, axiom208, axiom209, axiom21, axiom210, % 63.61/9.40 axiom211, axiom212, axiom213, axiom214, axiom215, axiom216, axiom217, axiom218, % 63.61/9.40 axiom219, axiom22, axiom220, axiom221, axiom222, axiom223, axiom224, axiom225, % 63.61/9.40 axiom226, axiom227, axiom228, axiom229, axiom23, axiom230, axiom231, axiom232, % 63.61/9.40 axiom233, axiom234, axiom235, axiom236, axiom237, axiom238, axiom239, axiom240, % 63.61/9.40 axiom241, axiom242, axiom243, axiom244, axiom245, axiom246, axiom247, axiom248, % 63.61/9.40 axiom249, axiom250, axiom251, axiom252, axiom253, axiom254, axiom255, axiom256, % 63.61/9.40 axiom257, axiom258, axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, % 63.61/9.40 axiom264, axiom265, axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, % 63.61/9.40 axiom271, axiom272, axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, % 63.61/9.40 axiom279, axiom280, axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, % 63.61/9.40 axiom287, axiom288, axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, % 63.61/9.40 axiom294, axiom295, axiom296, axiom297, axiom298, axiom299, axiom30, axiom300, % 63.61/9.40 axiom301, axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, % 63.61/9.40 axiom309, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, % 63.61/9.40 axiom317, axiom318, axiom319, axiom320, axiom321, axiom322, axiom323, axiom324, % 63.61/9.40 axiom325, axiom326, axiom327, axiom328, axiom329, axiom330, axiom331, axiom332, % 63.61/9.40 axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, % 63.61/9.40 axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, % 63.61/9.40 axiom348, axiom349, axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, % 63.61/9.40 axiom356, axiom357, axiom358, axiom359, axiom360, axiom361, axiom362, axiom363, % 63.61/9.40 axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom370, axiom371, % 63.61/9.40 axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, axiom378, axiom379, % 63.61/9.40 axiom380, axiom381, axiom382, axiom383, axiom384, axiom385, axiom386, axiom387, % 63.61/9.40 axiom388, axiom389, axiom39, axiom390, axiom391, axiom392, axiom393, axiom394, % 63.61/9.40 axiom395, axiom396, axiom397, axiom398, axiom399, axiom4, axiom40, axiom400, % 63.61/9.40 axiom401, axiom402, axiom403, axiom404, axiom405, axiom406, axiom407, axiom408, % 63.61/9.40 axiom409, axiom41, axiom410, axiom411, axiom412, axiom413, axiom414, axiom415, % 63.61/9.40 axiom416, axiom42, axiom43, axiom44, axiom45, axiom49, axiom50, axiom51, % 63.61/9.40 axiom52, axiom53, axiom54, axiom55, axiom59, axiom64, axiom65, axiom66, axiom67, % 63.61/9.40 axiom68, axiom69, axiom70, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, % 63.61/9.40 axiom77, axiom78, axiom79, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, % 63.61/9.40 axiom86, axiom87, axiom88, axiom89, axiom90, axiom91, axiom92, axiom93, axiom94, % 63.61/9.40 axiom95, axiom96, axiom97, axiom98, axiom99, formula_418, formula_419 % 63.61/9.40 % 63.61/9.40 Those formulas are unsatisfiable: % 63.61/9.40 --------------------------------- % 63.61/9.40 % 63.61/9.40 Begin of proof % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom5) implies: % 63.61/9.41 | (1) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : ? [v2: % 63.61/9.41 | A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : (mat$(one$) = v0 & % 63.61/9.41 | matrix_inv$(p$) = v2 & matrix_matrix_mult$(v3, a$) = v1 & % 63.61/9.41 | matrix_matrix_mult$(v2, p$) = v3 & matrix_matrix_mult$(v0, a$) = v1 & % 63.61/9.41 | A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & % 63.61/9.41 | A_n_vec_n_vec$(v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom6) implies: % 63.61/9.41 | (2) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : ? [v2: % 63.61/9.41 | A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : (mat$(one$) = v3 & % 63.61/9.41 | matrix_inv$(p$) = v0 & matrix_matrix_mult$(v0, v3) = v2 & % 63.61/9.41 | matrix_matrix_mult$(v0, v1) = v2 & matrix_matrix_mult$(p$, a$) = v1 & % 63.61/9.41 | A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & % 63.61/9.41 | A_n_vec_n_vec$(v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom7) implies: % 63.61/9.41 | (3) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : (mat$(one$) = v1 & % 63.61/9.41 | matrix_inv$(p$) = v0 & matrix_matrix_mult$(v0, v1) = a$ & % 63.61/9.41 | A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom8) implies: % 63.61/9.41 | (4) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.41 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v2 = v1 | ~ % 63.61/9.41 | (matrix_matrix_mult$(v0, v1) = v2) | ~ A_n_vec_n_vec$(v1))) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom9) implies: % 63.61/9.41 | (5) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.41 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v2 = v1 | ~ % 63.61/9.41 | (matrix_matrix_mult$(v1, v0) = v2) | ~ A_n_vec_n_vec$(v1))) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom10) implies: % 63.61/9.41 | (6) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : ? [v2: % 63.61/9.41 | A_n_vec_n_vec$] : ? [v3: A_n_vec_n_vec$] : (matrix_inv$(p$) = v0 & % 63.61/9.41 | matrix_matrix_mult$(v1, a$) = v2 & matrix_matrix_mult$(v0, v3) = v2 & % 63.61/9.41 | matrix_matrix_mult$(v0, p$) = v1 & matrix_matrix_mult$(p$, a$) = v3 & % 63.61/9.41 | A_n_vec_n_vec$(v3) & A_n_vec_n_vec$(v2) & A_n_vec_n_vec$(v1) & % 63.61/9.41 | A_n_vec_n_vec$(v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom11) implies: % 63.61/9.41 | (7) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & matrix_matrix_mult$(v0, % 63.61/9.41 | a$) = a$ & A_n_vec_n_vec$(v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom12) implies: % 63.61/9.41 | (8) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.41 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.41 | (matrix_matrix_mult$(v2, v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.41 | A_n_vec_n_vec$(v1) | ? [v3: A_n_vec_n_vec$] : ? [v4: % 63.61/9.41 | A_n_vec_n_vec$] : ((v4 = v2 & matrix_inv$(v1) = v2) | ( ~ (v3 = % 63.61/9.41 | v0) & matrix_matrix_mult$(v1, v2) = v3 & % 63.61/9.41 | A_n_vec_n_vec$(v3)))) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.41 | A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, v2) = v0) | ~ % 63.61/9.41 | A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v3: % 63.61/9.41 | A_n_vec_n_vec$] : ? [v4: A_n_vec_n_vec$] : ((v4 = v2 & % 63.61/9.41 | matrix_inv$(v1) = v2) | ( ~ (v3 = v0) & matrix_matrix_mult$(v2, % 63.61/9.41 | v1) = v3 & A_n_vec_n_vec$(v3))))) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom13) implies: % 63.61/9.41 | (9) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.41 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 63.61/9.41 | A_n_vec_n_vec$] : (v3 = v0 | ~ (matrix_matrix_mult$(v2, v1) = v3) % 63.61/9.41 | | ~ A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v4: % 63.61/9.41 | A_n_vec_n_vec$] : ( ~ (v4 = v0) & matrix_matrix_mult$(v1, v2) = % 63.61/9.41 | v4 & A_n_vec_n_vec$(v4))) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.41 | A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v3 = v0 | ~ % 63.61/9.41 | (matrix_matrix_mult$(v1, v2) = v3) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.41 | A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : ( ~ (v4 = v0) & % 63.61/9.41 | matrix_matrix_mult$(v2, v1) = v4 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.61/9.41 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.41 | (matrix_matrix_mult$(v2, v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.41 | A_n_vec_n_vec$(v1) | matrix_matrix_mult$(v1, v2) = v0) & ! [v1: % 63.61/9.41 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.41 | (matrix_matrix_mult$(v1, v2) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.41 | A_n_vec_n_vec$(v1) | matrix_matrix_mult$(v2, v1) = v0)) % 63.61/9.41 | % 63.61/9.41 | ALPHA: (axiom14) implies: % 63.61/9.42 | (10) ? [v0: A_n_vec_n_vec$] : (gauss_Jordan$(a$) = v0 & % 63.61/9.42 | matrix_matrix_mult$(p$, a$) = v0 & A_n_vec_n_vec$(v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom15) implies: % 63.61/9.42 | (11) ? [v0: A_n_vec_n_vec$] : (gauss_Jordan$(a$) = v0 & mat$(one$) = v0 & % 63.61/9.42 | A_n_vec_n_vec$(v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom16) implies: % 63.61/9.42 | (12) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : (gauss_Jordan$(a$) % 63.61/9.42 | = v0 & matrix_matrix_mult$(v1, a$) = v0 & A_n_vec_n_vec$(v1) & % 63.61/9.42 | A_n_vec_n_vec$(v0) & fun_app$(invertible$, v1)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom18) implies: % 63.61/9.42 | (13) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (matrix_matrix_mult$(v1, v2) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.42 | A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1)) & ! [v1: % 63.61/9.42 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ~ % 63.61/9.42 | fun_app$(invertible$, v1) | ? [v2: A_n_vec_n_vec$] : % 63.61/9.42 | (matrix_matrix_mult$(v1, v2) = v0 & A_n_vec_n_vec$(v2)))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom19) implies: % 63.61/9.42 | (14) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (matrix_matrix_mult$(v2, v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.42 | A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1) | ? [v3: % 63.61/9.42 | A_n_vec_n_vec$] : ( ~ (v3 = v0) & matrix_matrix_mult$(v1, v2) = % 63.61/9.42 | v3 & A_n_vec_n_vec$(v3))) & ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.42 | A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v1, v2) = v0) | ~ % 63.61/9.42 | A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v1) | fun_app$(invertible$, % 63.61/9.42 | v1) | ? [v3: A_n_vec_n_vec$] : ( ~ (v3 = v0) & % 63.61/9.42 | matrix_matrix_mult$(v2, v1) = v3 & A_n_vec_n_vec$(v3))) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ~ % 63.61/9.42 | fun_app$(invertible$, v1) | ? [v2: A_n_vec_n_vec$] : % 63.61/9.42 | (matrix_matrix_mult$(v2, v1) = v0 & matrix_matrix_mult$(v1, v2) = % 63.61/9.42 | v0 & A_n_vec_n_vec$(v2)))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom20) implies: % 63.61/9.42 | (15) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (matrix_matrix_mult$(v2, v1) = v0) | ~ A_n_vec_n_vec$(v2) | ~ % 63.61/9.42 | A_n_vec_n_vec$(v1) | fun_app$(invertible$, v1)) & ! [v1: % 63.61/9.42 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ~ % 63.61/9.42 | fun_app$(invertible$, v1) | ? [v2: A_n_vec_n_vec$] : % 63.61/9.42 | (matrix_matrix_mult$(v2, v1) = v0 & A_n_vec_n_vec$(v2)))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom24) implies: % 63.61/9.42 | (16) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (matrix_inv$(v1) = v2) | ~ A_n_vec_n_vec$(v1) | ~ % 63.61/9.42 | fun_app$(invertible$, v1) | matrix_matrix_mult$(v1, v2) = v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom25) implies: % 63.61/9.42 | (17) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (matrix_inv$(v1) = v2) | ~ A_n_vec_n_vec$(v1) | ~ % 63.61/9.42 | fun_app$(invertible$, v1) | matrix_matrix_mult$(v2, v1) = v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom28) implies: % 63.61/9.42 | (18) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.61/9.42 | fun_app$(invertible$, v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom31) implies: % 63.61/9.42 | (19) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & % 63.61/9.42 | fun_app$(orthogonal_matrix$, v0)) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom32) implies: % 63.61/9.42 | (20) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : (v2 % 63.61/9.42 | = v1 | ~ (column_add$(v0, v1, v2, v3) = v4) | ~ A$(v3) | ~ % 63.61/9.42 | N$(v2) | ~ N$(v1) | fun_app$(invertible$, v4))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom33) implies: % 63.61/9.42 | (21) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A$] : ! % 63.61/9.42 | [v5: A_n_vec_n_vec$] : ! [v6: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (column_add$(v0, v2, v3, v4) = v5) | ~ (matrix_matrix_mult$(v1, % 63.61/9.42 | v5) = v6) | ~ A$(v4) | ~ N$(v3) | ~ N$(v2) | ~ % 63.61/9.42 | A_n_vec_n_vec$(v1) | (column_add$(v1, v2, v3, v4) = v6 & % 63.61/9.42 | A_n_vec_n_vec$(v6))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : % 63.61/9.42 | ! [v3: N$] : ! [v4: A$] : ! [v5: A_n_vec_n_vec$] : ( ~ % 63.61/9.42 | (column_add$(v1, v2, v3, v4) = v5) | ~ A$(v4) | ~ N$(v3) | ~ % 63.61/9.42 | N$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v6: A_n_vec_n_vec$] : % 63.61/9.42 | (column_add$(v0, v2, v3, v4) = v6 & matrix_matrix_mult$(v1, v6) = % 63.61/9.42 | v5 & A_n_vec_n_vec$(v6) & A_n_vec_n_vec$(v5)))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom35) implies: % 63.61/9.42 | (22) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.42 | [v1: A_n_vec$] : ! [v2: A_n_vec$] : (v2 = v1 | ~ % 63.61/9.42 | (vector_matrix_mult$a(v1, v0) = v2) | ~ A_n_vec$(v1))) % 63.61/9.42 | % 63.61/9.42 | ALPHA: (axiom36) implies: % 63.61/9.43 | (23) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: A$] : ! [v4: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ (mult_column$(v0, % 63.61/9.43 | v2, v3) = v4) | ~ (matrix_matrix_mult$(v1, v4) = v5) | ~ % 63.61/9.43 | A$(v3) | ~ N$(v2) | ~ A_n_vec_n_vec$(v1) | (mult_column$(v1, v2, % 63.61/9.43 | v3) = v5 & A_n_vec_n_vec$(v5))) & ! [v1: A_n_vec_n_vec$] : ! % 63.61/9.43 | [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.61/9.43 | (mult_column$(v1, v2, v3) = v4) | ~ A$(v3) | ~ N$(v2) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | ? [v5: A_n_vec_n_vec$] : (mult_column$(v0, % 63.61/9.43 | v2, v3) = v5 & matrix_matrix_mult$(v1, v5) = v4 & % 63.61/9.43 | A_n_vec_n_vec$(v5) & A_n_vec_n_vec$(v4)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom37) implies: % 63.61/9.43 | (24) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: N$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ % 63.61/9.43 | (interchange_columns$(v0, v1, v2) = v3) | ~ N$(v2) | ~ N$(v1) | % 63.61/9.43 | fun_app$(invertible$, v3))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom38) implies: % 63.61/9.43 | (25) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.61/9.43 | (matrix_matrix_mult$(v3, v1) = v0) | ~ A_n_vec_n_vec$(v3) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.61/9.43 | (matrix_matrix_mult$(v2, v4) = v0 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.61/9.43 | (matrix_matrix_mult$(v2, v3) = v0) | ~ A_n_vec_n_vec$(v3) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.61/9.43 | (matrix_matrix_mult$(v4, v1) = v0 & A_n_vec_n_vec$(v4)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom46) implies: % 63.61/9.43 | (26) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v1) % 63.61/9.43 | = v2) | ~ A_n_vec_n_vec$(v1) | ~ fun_app$(orthogonal_matrix$, % 63.61/9.43 | v1) | (matrix_matrix_mult$(v2, v1) = v0 & % 63.61/9.43 | matrix_matrix_mult$(v1, v2) = v0)) & ! [v1: A_n_vec_n_vec$] : % 63.61/9.43 | ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | fun_app$(orthogonal_matrix$, v1) | ? [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ? [v4: A_n_vec_n_vec$] : (( ~ (v4 = v0) & % 63.61/9.43 | matrix_matrix_mult$(v1, v2) = v4 & A_n_vec_n_vec$(v4)) | ( ~ % 63.61/9.43 | (v3 = v0) & matrix_matrix_mult$(v2, v1) = v3 & % 63.61/9.43 | A_n_vec_n_vec$(v3))))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom47) implies: % 63.61/9.43 | (27) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ % 63.61/9.43 | (interchange_columns$(v0, v2, v3) = v4) | ~ % 63.61/9.43 | (matrix_matrix_mult$(v1, v4) = v5) | ~ N$(v3) | ~ N$(v2) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | (interchange_columns$(v1, v2, v3) = v5 & % 63.61/9.43 | A_n_vec_n_vec$(v5))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : % 63.61/9.43 | ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : ( ~ (interchange_columns$(v1, % 63.61/9.43 | v2, v3) = v4) | ~ N$(v3) | ~ N$(v2) | ~ A_n_vec_n_vec$(v1) % 63.61/9.43 | | ? [v5: A_n_vec_n_vec$] : (interchange_columns$(v0, v2, v3) = v5 % 63.61/9.43 | & matrix_matrix_mult$(v1, v5) = v4 & A_n_vec_n_vec$(v5) & % 63.61/9.43 | A_n_vec_n_vec$(v4)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom48) implies: % 63.61/9.43 | (28) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.61/9.43 | (matrix_matrix_mult$(v3, v2) = v0) | ~ A_n_vec_n_vec$(v3) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.61/9.43 | (matrix_matrix_mult$(v1, v4) = v0 & A_n_vec_n_vec$(v4))) & ! [v1: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ( ~ (transpose$(v1) = v2) | ~ % 63.61/9.43 | (matrix_matrix_mult$(v1, v3) = v0) | ~ A_n_vec_n_vec$(v3) | ~ % 63.61/9.43 | A_n_vec_n_vec$(v1) | ? [v4: A_n_vec_n_vec$] : % 63.61/9.43 | (matrix_matrix_mult$(v4, v2) = v0 & A_n_vec_n_vec$(v4)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom56) implies: % 63.61/9.43 | (29) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = zero$ | ~ % 63.61/9.43 | (mult_column$(v0, v2, v1) = v3) | ~ A$(v1) | ~ N$(v2) | % 63.61/9.43 | fun_app$(invertible$, v3))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom57) implies: % 63.61/9.43 | (30) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : ! [v4: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ (mult_row$(v0, v1, % 63.61/9.43 | v2) = v4) | ~ (matrix_matrix_mult$(v4, v3) = v5) | ~ A$(v2) % 63.61/9.43 | | ~ N$(v1) | ~ A_n_vec_n_vec$(v3) | (mult_row$(v3, v1, v2) = v5 % 63.61/9.43 | & A_n_vec_n_vec$(v5))) & ! [v1: N$] : ! [v2: A$] : ! [v3: % 63.61/9.43 | A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] : ( ~ (mult_row$(v3, v1, % 63.61/9.43 | v2) = v4) | ~ A$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v3) | ? % 63.61/9.43 | [v5: A_n_vec_n_vec$] : (mult_row$(v0, v1, v2) = v5 & % 63.61/9.43 | matrix_matrix_mult$(v5, v3) = v4 & A_n_vec_n_vec$(v5) & % 63.61/9.43 | A_n_vec_n_vec$(v4)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom58) implies: % 63.61/9.43 | (31) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.61/9.43 | (times$(v2, v1) = one$) | ~ (mult_column$(v0, v3, v1) = v4) | ~ % 63.61/9.43 | A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, v4) | ? % 63.61/9.43 | [v5: A$] : ( ~ (v5 = one$) & times$(v1, v2) = v5 & A$(v5))) & ! % 63.61/9.43 | [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.61/9.43 | (times$(v1, v2) = one$) | ~ (mult_column$(v0, v3, v1) = v4) | ~ % 63.61/9.43 | A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, v4) | ? % 63.61/9.43 | [v5: A$] : ( ~ (v5 = one$) & times$(v2, v1) = v5 & A$(v5)))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom60) implies: % 63.61/9.43 | (32) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.43 | [v1: N$] : ! [v2: N$] : ! [v3: N_a_n_vec_n_vec_fun$] : ! [v4: % 63.61/9.43 | A_n_vec_n_vec$] : ( ~ (interchange_rows$(v0, v1) = v3) | ~ % 63.61/9.43 | (fun_app$c(v3, v2) = v4) | ~ N$(v2) | ~ N$(v1) | % 63.61/9.43 | fun_app$(invertible$, v4))) % 63.61/9.43 | % 63.61/9.43 | ALPHA: (axiom61) implies: % 63.61/9.44 | (33) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: N$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ! [v4: % 63.61/9.44 | N_a_n_vec_n_vec_fun$] : ! [v5: A_n_vec_n_vec$] : ! [v6: % 63.61/9.44 | A_n_vec_n_vec$] : ( ~ (interchange_rows$(v0, v1) = v4) | ~ % 63.61/9.44 | (fun_app$c(v4, v2) = v5) | ~ (matrix_matrix_mult$(v5, v3) = v6) | % 63.61/9.44 | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v3) | ? [v7: % 63.61/9.44 | N_a_n_vec_n_vec_fun$] : (interchange_rows$(v3, v1) = v7 & % 63.61/9.44 | fun_app$c(v7, v2) = v6 & N_a_n_vec_n_vec_fun$(v7) & % 63.61/9.44 | A_n_vec_n_vec$(v6))) & ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.61/9.44 | A_n_vec_n_vec$] : ! [v4: N_a_n_vec_n_vec_fun$] : ! [v5: % 63.61/9.44 | A_n_vec_n_vec$] : ( ~ (interchange_rows$(v3, v1) = v4) | ~ % 63.61/9.44 | (fun_app$c(v4, v2) = v5) | ~ N$(v2) | ~ N$(v1) | ~ % 63.61/9.44 | A_n_vec_n_vec$(v3) | ? [v6: N_a_n_vec_n_vec_fun$] : ? [v7: % 63.61/9.44 | A_n_vec_n_vec$] : (interchange_rows$(v0, v1) = v6 & % 63.61/9.44 | fun_app$c(v6, v2) = v7 & matrix_matrix_mult$(v7, v3) = v5 & % 63.61/9.44 | N_a_n_vec_n_vec_fun$(v6) & A_n_vec_n_vec$(v7) & % 63.61/9.44 | A_n_vec_n_vec$(v5)))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom62) implies: % 63.61/9.44 | (34) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : (v2 % 63.61/9.44 | = v1 | ~ (row_add$(v0, v1, v2, v3) = v4) | ~ A$(v3) | ~ N$(v2) % 63.61/9.44 | | ~ N$(v1) | fun_app$(invertible$, v4))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom63) implies: % 63.61/9.44 | (35) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : ! % 63.61/9.44 | [v5: A_n_vec_n_vec$] : ! [v6: A_n_vec_n_vec$] : ( ~ (row_add$(v0, % 63.61/9.44 | v1, v2, v3) = v5) | ~ (matrix_matrix_mult$(v5, v4) = v6) | ~ % 63.61/9.44 | A$(v3) | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v4) | % 63.61/9.44 | (row_add$(v4, v1, v2, v3) = v6 & A_n_vec_n_vec$(v6))) & ! [v1: % 63.61/9.44 | N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : ! % 63.61/9.44 | [v5: A_n_vec_n_vec$] : ( ~ (row_add$(v4, v1, v2, v3) = v5) | ~ % 63.61/9.44 | A$(v3) | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v4) | ? [v6: % 63.61/9.44 | A_n_vec_n_vec$] : (row_add$(v0, v1, v2, v3) = v6 & % 63.61/9.44 | matrix_matrix_mult$(v6, v4) = v5 & A_n_vec_n_vec$(v6) & % 63.61/9.44 | A_n_vec_n_vec$(v5)))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom122) implies: % 63.61/9.44 | (36) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.61/9.44 | (times$(v2, v1) = one$) | ~ (mult_row$(v0, v3, v1) = v4) | ~ % 63.61/9.44 | A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, v4) | ? % 63.61/9.44 | [v5: A$] : ( ~ (v5 = one$) & times$(v1, v2) = v5 & A$(v5))) & ! % 63.61/9.44 | [v1: A$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.61/9.44 | (times$(v1, v2) = one$) | ~ (mult_row$(v0, v3, v1) = v4) | ~ % 63.61/9.44 | A$(v2) | ~ A$(v1) | ~ N$(v3) | fun_app$(invertible$, v4) | ? % 63.61/9.44 | [v5: A$] : ( ~ (v5 = one$) & times$(v2, v1) = v5 & A$(v5)))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom123) implies: % 63.61/9.44 | (37) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = zero$ | ~ % 63.61/9.44 | (mult_row$(v0, v2, v1) = v3) | ~ A$(v1) | ~ N$(v2) | % 63.61/9.44 | fun_app$(invertible$, v3))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom159) implies: % 63.61/9.44 | (38) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_n_vec$] : % 63.61/9.44 | (v2 = zero$c | ~ (matrix_vector_mult$(v1, v2) = zero$c) | ~ % 63.61/9.44 | (matrix_matrix_mult$(v3, v1) = v0) | ~ A_n_vec$(v2) | ~ % 63.61/9.44 | A_n_vec_n_vec$(v3) | ~ A_n_vec_n_vec$(v1)) & ? [v1: % 63.61/9.44 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v1) | ? [v2: A_n_vec_n_vec$] % 63.61/9.44 | : ? [v3: A_n_vec_n_vec$] : ? [v4: A_n_vec$] : ? [v5: A_n_vec$] % 63.61/9.44 | : (A_n_vec$(v4) & A_n_vec_n_vec$(v2) & ((v5 = zero$c & ~ (v4 = % 63.61/9.44 | zero$c) & matrix_vector_mult$(v1, v4) = zero$c) | (v3 = v0 % 63.61/9.44 | & matrix_matrix_mult$(v2, v1) = v0))))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (axiom179) implies: % 63.61/9.44 | (39) ? [v0: A_n_vec_n_vec$] : (mat$(one$) = v0 & A_n_vec_n_vec$(v0) & ! % 63.61/9.44 | [v1: A_n_vec$] : ! [v2: A_n_vec$] : (v2 = v1 | ~ % 63.61/9.44 | (matrix_vector_mult$(v0, v1) = v2) | ~ A_n_vec$(v1))) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (conjecture3) implies: % 63.61/9.44 | (40) ? [v0: A_n_vec_n_vec$] : ? [v1: A_n_vec_n_vec$] : ? [v2: % 63.61/9.44 | A_n_vec_n_vec$] : ( ~ (v2 = v0) & mat$(one$) = v1 & matrix_inv$(p$) % 63.61/9.44 | = v0 & matrix_matrix_mult$(v0, v1) = v2 & A_n_vec_n_vec$(v2) & % 63.61/9.44 | A_n_vec_n_vec$(v1) & A_n_vec_n_vec$(v0)) % 63.61/9.44 | % 63.61/9.44 | ALPHA: (function-axioms) implies: % 63.61/9.44 | (41) ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.44 | A_n_vec_n_vec$] : (v1 = v0 | ~ (matrix_inv$(v2) = v1) | ~ % 63.61/9.44 | (matrix_inv$(v2) = v0)) % 63.61/9.44 | (42) ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A$] : (v1 % 63.61/9.44 | = v0 | ~ (mat$(v2) = v1) | ~ (mat$(v2) = v0)) % 63.61/9.44 | (43) ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.44 | A_n_vec_n_vec$] : (v1 = v0 | ~ (gauss_Jordan$(v2) = v1) | ~ % 63.61/9.44 | (gauss_Jordan$(v2) = v0)) % 63.61/9.45 | (44) ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 63.61/9.45 | A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.45 | (matrix_matrix_mult$(v3, v2) = v1) | ~ (matrix_matrix_mult$(v3, v2) % 63.61/9.45 | = v0)) % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (19) with fresh symbol all_396_0 gives: % 63.61/9.45 | (45) mat$(one$) = all_396_0 & A_n_vec_n_vec$(all_396_0) & % 63.61/9.45 | fun_app$(orthogonal_matrix$, all_396_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (45) implies: % 63.61/9.45 | (46) mat$(one$) = all_396_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (7) with fresh symbol all_398_0 gives: % 63.61/9.45 | (47) mat$(one$) = all_398_0 & matrix_matrix_mult$(all_398_0, a$) = a$ & % 63.61/9.45 | A_n_vec_n_vec$(all_398_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (47) implies: % 63.61/9.45 | (48) matrix_matrix_mult$(all_398_0, a$) = a$ % 63.61/9.45 | (49) mat$(one$) = all_398_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (11) with fresh symbol all_400_0 gives: % 63.61/9.45 | (50) gauss_Jordan$(a$) = all_400_0 & mat$(one$) = all_400_0 & % 63.61/9.45 | A_n_vec_n_vec$(all_400_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (50) implies: % 63.61/9.45 | (51) mat$(one$) = all_400_0 % 63.61/9.45 | (52) gauss_Jordan$(a$) = all_400_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (10) with fresh symbol all_402_0 gives: % 63.61/9.45 | (53) gauss_Jordan$(a$) = all_402_0 & matrix_matrix_mult$(p$, a$) = % 63.61/9.45 | all_402_0 & A_n_vec_n_vec$(all_402_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (53) implies: % 63.61/9.45 | (54) matrix_matrix_mult$(p$, a$) = all_402_0 % 63.61/9.45 | (55) gauss_Jordan$(a$) = all_402_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (18) with fresh symbol all_404_0 gives: % 63.61/9.45 | (56) mat$(one$) = all_404_0 & A_n_vec_n_vec$(all_404_0) & % 63.61/9.45 | fun_app$(invertible$, all_404_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (56) implies: % 63.61/9.45 | (57) mat$(one$) = all_404_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (3) with fresh symbols all_413_0, all_413_1 gives: % 63.61/9.45 | (58) mat$(one$) = all_413_0 & matrix_inv$(p$) = all_413_1 & % 63.61/9.45 | matrix_matrix_mult$(all_413_1, all_413_0) = a$ & % 63.61/9.45 | A_n_vec_n_vec$(all_413_0) & A_n_vec_n_vec$(all_413_1) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (58) implies: % 63.61/9.45 | (59) matrix_inv$(p$) = all_413_1 % 63.61/9.45 | (60) mat$(one$) = all_413_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (12) with fresh symbols all_417_0, all_417_1 gives: % 63.61/9.45 | (61) gauss_Jordan$(a$) = all_417_1 & matrix_matrix_mult$(all_417_0, a$) = % 63.61/9.45 | all_417_1 & A_n_vec_n_vec$(all_417_0) & A_n_vec_n_vec$(all_417_1) & % 63.61/9.45 | fun_app$(invertible$, all_417_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (61) implies: % 63.61/9.45 | (62) gauss_Jordan$(a$) = all_417_1 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (5) with fresh symbol all_419_0 gives: % 63.61/9.45 | (63) mat$(one$) = all_419_0 & A_n_vec_n_vec$(all_419_0) & ! [v0: % 63.61/9.45 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.45 | (matrix_matrix_mult$(v0, all_419_0) = v1) | ~ A_n_vec_n_vec$(v0)) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (63) implies: % 63.61/9.45 | (64) mat$(one$) = all_419_0 % 63.61/9.45 | (65) ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.45 | (matrix_matrix_mult$(v0, all_419_0) = v1) | ~ A_n_vec_n_vec$(v0)) % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (22) with fresh symbol all_426_0 gives: % 63.61/9.45 | (66) mat$(one$) = all_426_0 & A_n_vec_n_vec$(all_426_0) & ! [v0: A_n_vec$] % 63.61/9.45 | : ! [v1: A_n_vec$] : (v1 = v0 | ~ (vector_matrix_mult$a(v0, % 63.61/9.45 | all_426_0) = v1) | ~ A_n_vec$(v0)) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (66) implies: % 63.61/9.45 | (67) mat$(one$) = all_426_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (39) with fresh symbol all_429_0 gives: % 63.61/9.45 | (68) mat$(one$) = all_429_0 & A_n_vec_n_vec$(all_429_0) & ! [v0: A_n_vec$] % 63.61/9.45 | : ! [v1: A_n_vec$] : (v1 = v0 | ~ (matrix_vector_mult$(all_429_0, % 63.61/9.45 | v0) = v1) | ~ A_n_vec$(v0)) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (68) implies: % 63.61/9.45 | (69) mat$(one$) = all_429_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (4) with fresh symbol all_435_0 gives: % 63.61/9.45 | (70) mat$(one$) = all_435_0 & A_n_vec_n_vec$(all_435_0) & ! [v0: % 63.61/9.45 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.45 | (matrix_matrix_mult$(all_435_0, v0) = v1) | ~ A_n_vec_n_vec$(v0)) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (70) implies: % 63.61/9.45 | (71) mat$(one$) = all_435_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (16) with fresh symbol all_438_0 gives: % 63.61/9.45 | (72) mat$(one$) = all_438_0 & A_n_vec_n_vec$(all_438_0) & ! [v0: % 63.61/9.45 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ (matrix_inv$(v0) = % 63.61/9.45 | v1) | ~ A_n_vec_n_vec$(v0) | ~ fun_app$(invertible$, v0) | % 63.61/9.45 | matrix_matrix_mult$(v0, v1) = all_438_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (72) implies: % 63.61/9.45 | (73) mat$(one$) = all_438_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (17) with fresh symbol all_441_0 gives: % 63.61/9.45 | (74) mat$(one$) = all_441_0 & A_n_vec_n_vec$(all_441_0) & ! [v0: % 63.61/9.45 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ (matrix_inv$(v0) = % 63.61/9.45 | v1) | ~ A_n_vec_n_vec$(v0) | ~ fun_app$(invertible$, v0) | % 63.61/9.45 | matrix_matrix_mult$(v1, v0) = all_441_0) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (74) implies: % 63.61/9.45 | (75) mat$(one$) = all_441_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (24) with fresh symbol all_444_0 gives: % 63.61/9.45 | (76) mat$(one$) = all_444_0 & A_n_vec_n_vec$(all_444_0) & ! [v0: N$] : ! % 63.61/9.45 | [v1: N$] : ! [v2: A_n_vec_n_vec$] : ( ~ % 63.61/9.45 | (interchange_columns$(all_444_0, v0, v1) = v2) | ~ N$(v1) | ~ % 63.61/9.45 | N$(v0) | fun_app$(invertible$, v2)) % 63.61/9.45 | % 63.61/9.45 | ALPHA: (76) implies: % 63.61/9.45 | (77) mat$(one$) = all_444_0 % 63.61/9.45 | % 63.61/9.45 | DELTA: instantiating (40) with fresh symbols all_447_0, all_447_1, all_447_2 % 63.61/9.45 | gives: % 63.61/9.46 | (78) ~ (all_447_0 = all_447_2) & mat$(one$) = all_447_1 & matrix_inv$(p$) % 63.61/9.46 | = all_447_2 & matrix_matrix_mult$(all_447_2, all_447_1) = all_447_0 & % 63.61/9.46 | A_n_vec_n_vec$(all_447_0) & A_n_vec_n_vec$(all_447_1) & % 63.61/9.46 | A_n_vec_n_vec$(all_447_2) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (78) implies: % 63.61/9.46 | (79) ~ (all_447_0 = all_447_2) % 63.61/9.46 | (80) A_n_vec_n_vec$(all_447_2) % 63.61/9.46 | (81) matrix_matrix_mult$(all_447_2, all_447_1) = all_447_0 % 63.61/9.46 | (82) matrix_inv$(p$) = all_447_2 % 63.61/9.46 | (83) mat$(one$) = all_447_1 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (29) with fresh symbol all_449_0 gives: % 63.61/9.46 | (84) mat$(one$) = all_449_0 & A_n_vec_n_vec$(all_449_0) & ! [v0: A$] : ! % 63.61/9.46 | [v1: N$] : ! [v2: A_n_vec_n_vec$] : (v0 = zero$ | ~ % 63.61/9.46 | (mult_column$(all_449_0, v1, v0) = v2) | ~ A$(v0) | ~ N$(v1) | % 63.61/9.46 | fun_app$(invertible$, v2)) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (84) implies: % 63.61/9.46 | (85) mat$(one$) = all_449_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (37) with fresh symbol all_452_0 gives: % 63.61/9.46 | (86) mat$(one$) = all_452_0 & A_n_vec_n_vec$(all_452_0) & ! [v0: A$] : ! % 63.61/9.46 | [v1: N$] : ! [v2: A_n_vec_n_vec$] : (v0 = zero$ | ~ % 63.61/9.46 | (mult_row$(all_452_0, v1, v0) = v2) | ~ A$(v0) | ~ N$(v1) | % 63.61/9.46 | fun_app$(invertible$, v2)) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (86) implies: % 63.61/9.46 | (87) mat$(one$) = all_452_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (32) with fresh symbol all_455_0 gives: % 63.61/9.46 | (88) mat$(one$) = all_455_0 & A_n_vec_n_vec$(all_455_0) & ! [v0: N$] : ! % 63.61/9.46 | [v1: N$] : ! [v2: N_a_n_vec_n_vec_fun$] : ! [v3: A_n_vec_n_vec$] : ( % 63.61/9.46 | ~ (interchange_rows$(all_455_0, v0) = v2) | ~ (fun_app$c(v2, v1) = % 63.61/9.46 | v3) | ~ N$(v1) | ~ N$(v0) | fun_app$(invertible$, v3)) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (88) implies: % 63.61/9.46 | (89) mat$(one$) = all_455_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (34) with fresh symbol all_458_0 gives: % 63.61/9.46 | (90) mat$(one$) = all_458_0 & A_n_vec_n_vec$(all_458_0) & ! [v0: N$] : ! % 63.61/9.46 | [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.46 | (row_add$(all_458_0, v0, v1, v2) = v3) | ~ A$(v2) | ~ N$(v1) | ~ % 63.61/9.46 | N$(v0) | fun_app$(invertible$, v3)) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (90) implies: % 63.61/9.46 | (91) mat$(one$) = all_458_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (20) with fresh symbol all_461_0 gives: % 63.61/9.46 | (92) mat$(one$) = all_461_0 & A_n_vec_n_vec$(all_461_0) & ! [v0: N$] : ! % 63.61/9.46 | [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 63.61/9.46 | (column_add$(all_461_0, v0, v1, v2) = v3) | ~ A$(v2) | ~ N$(v1) | % 63.61/9.46 | ~ N$(v0) | fun_app$(invertible$, v3)) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (92) implies: % 63.61/9.46 | (93) mat$(one$) = all_461_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (2) with fresh symbols all_464_0, all_464_1, all_464_2, % 63.61/9.46 | all_464_3 gives: % 63.61/9.46 | (94) mat$(one$) = all_464_0 & matrix_inv$(p$) = all_464_3 & % 63.61/9.46 | matrix_matrix_mult$(all_464_3, all_464_0) = all_464_1 & % 63.61/9.46 | matrix_matrix_mult$(all_464_3, all_464_2) = all_464_1 & % 63.61/9.46 | matrix_matrix_mult$(p$, a$) = all_464_2 & A_n_vec_n_vec$(all_464_0) & % 63.61/9.46 | A_n_vec_n_vec$(all_464_1) & A_n_vec_n_vec$(all_464_2) & % 63.61/9.46 | A_n_vec_n_vec$(all_464_3) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (94) implies: % 63.61/9.46 | (95) matrix_matrix_mult$(p$, a$) = all_464_2 % 63.61/9.46 | (96) matrix_matrix_mult$(all_464_3, all_464_2) = all_464_1 % 63.61/9.46 | (97) matrix_inv$(p$) = all_464_3 % 63.61/9.46 | (98) mat$(one$) = all_464_0 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (1) with fresh symbols all_467_0, all_467_1, all_467_2, % 63.61/9.46 | all_467_3 gives: % 63.61/9.46 | (99) mat$(one$) = all_467_3 & matrix_inv$(p$) = all_467_1 & % 63.61/9.46 | matrix_matrix_mult$(all_467_0, a$) = all_467_2 & % 63.61/9.46 | matrix_matrix_mult$(all_467_1, p$) = all_467_0 & % 63.61/9.46 | matrix_matrix_mult$(all_467_3, a$) = all_467_2 & % 63.61/9.46 | A_n_vec_n_vec$(all_467_0) & A_n_vec_n_vec$(all_467_1) & % 63.61/9.46 | A_n_vec_n_vec$(all_467_2) & A_n_vec_n_vec$(all_467_3) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (99) implies: % 63.61/9.46 | (100) matrix_matrix_mult$(all_467_3, a$) = all_467_2 % 63.61/9.46 | (101) matrix_matrix_mult$(all_467_1, p$) = all_467_0 % 63.61/9.46 | (102) matrix_matrix_mult$(all_467_0, a$) = all_467_2 % 63.61/9.46 | (103) matrix_inv$(p$) = all_467_1 % 63.61/9.46 | (104) mat$(one$) = all_467_3 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (6) with fresh symbols all_470_0, all_470_1, all_470_2, % 63.61/9.46 | all_470_3 gives: % 63.61/9.46 | (105) matrix_inv$(p$) = all_470_3 & matrix_matrix_mult$(all_470_2, a$) = % 63.61/9.46 | all_470_1 & matrix_matrix_mult$(all_470_3, all_470_0) = all_470_1 & % 63.61/9.46 | matrix_matrix_mult$(all_470_3, p$) = all_470_2 & % 63.61/9.46 | matrix_matrix_mult$(p$, a$) = all_470_0 & A_n_vec_n_vec$(all_470_0) & % 63.61/9.46 | A_n_vec_n_vec$(all_470_1) & A_n_vec_n_vec$(all_470_2) & % 63.61/9.46 | A_n_vec_n_vec$(all_470_3) % 63.61/9.46 | % 63.61/9.46 | ALPHA: (105) implies: % 63.61/9.46 | (106) matrix_matrix_mult$(p$, a$) = all_470_0 % 63.61/9.46 | (107) matrix_matrix_mult$(all_470_3, p$) = all_470_2 % 63.61/9.46 | (108) matrix_matrix_mult$(all_470_3, all_470_0) = all_470_1 % 63.61/9.46 | (109) matrix_matrix_mult$(all_470_2, a$) = all_470_1 % 63.61/9.46 | (110) matrix_inv$(p$) = all_470_3 % 63.61/9.46 | % 63.61/9.46 | DELTA: instantiating (13) with fresh symbol all_472_0 gives: % 63.61/9.46 | (111) mat$(one$) = all_472_0 & A_n_vec_n_vec$(all_472_0) & ! [v0: % 63.61/9.46 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 63.61/9.46 | (matrix_matrix_mult$(v0, v1) = all_472_0) | ~ A_n_vec_n_vec$(v1) | % 63.61/9.46 | ~ A_n_vec_n_vec$(v0) | fun_app$(invertible$, v0)) & ! [v0: % 63.61/9.47 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v0) | ~ fun_app$(invertible$, % 63.61/9.47 | v0) | ? [v1: A_n_vec_n_vec$] : (matrix_matrix_mult$(v0, v1) = % 63.61/9.47 | all_472_0 & A_n_vec_n_vec$(v1))) % 63.61/9.47 | % 63.61/9.47 | ALPHA: (111) implies: % 63.61/9.47 | (112) mat$(one$) = all_472_0 % 63.61/9.47 | % 63.61/9.47 | DELTA: instantiating (15) with fresh symbol all_475_0 gives: % 63.61/9.47 | (113) mat$(one$) = all_475_0 & A_n_vec_n_vec$(all_475_0) & ! [v0: % 63.61/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 63.61/9.47 | (matrix_matrix_mult$(v1, v0) = all_475_0) | ~ A_n_vec_n_vec$(v1) | % 63.61/9.47 | ~ A_n_vec_n_vec$(v0) | fun_app$(invertible$, v0)) & ! [v0: % 63.61/9.47 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v0) | ~ fun_app$(invertible$, % 63.61/9.47 | v0) | ? [v1: A_n_vec_n_vec$] : (matrix_matrix_mult$(v1, v0) = % 63.61/9.47 | all_475_0 & A_n_vec_n_vec$(v1))) % 63.61/9.47 | % 63.61/9.47 | ALPHA: (113) implies: % 63.61/9.47 | (114) mat$(one$) = all_475_0 % 63.61/9.47 | % 63.61/9.47 | DELTA: instantiating (25) with fresh symbol all_486_0 gives: % 63.61/9.47 | (115) mat$(one$) = all_486_0 & A_n_vec_n_vec$(all_486_0) & ! [v0: % 63.61/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] % 63.61/9.47 | : ( ~ (transpose$(v0) = v1) | ~ (matrix_matrix_mult$(v2, v0) = % 63.61/9.47 | all_486_0) | ~ A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v0) | ? % 63.61/9.47 | [v3: A_n_vec_n_vec$] : (matrix_matrix_mult$(v1, v3) = all_486_0 & % 63.61/9.47 | A_n_vec_n_vec$(v3))) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.47 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v0) = % 63.61/9.47 | v1) | ~ (matrix_matrix_mult$(v1, v2) = all_486_0) | ~ % 63.61/9.47 | A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v0) | ? [v3: % 63.61/9.47 | A_n_vec_n_vec$] : (matrix_matrix_mult$(v3, v0) = all_486_0 & % 63.61/9.47 | A_n_vec_n_vec$(v3))) % 63.61/9.47 | % 63.61/9.47 | ALPHA: (115) implies: % 63.61/9.47 | (116) mat$(one$) = all_486_0 % 63.61/9.47 | % 63.61/9.47 | DELTA: instantiating (28) with fresh symbol all_489_0 gives: % 63.61/9.47 | (117) mat$(one$) = all_489_0 & A_n_vec_n_vec$(all_489_0) & ! [v0: % 63.61/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] % 63.61/9.47 | : ( ~ (transpose$(v0) = v1) | ~ (matrix_matrix_mult$(v2, v1) = % 63.61/9.47 | all_489_0) | ~ A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v0) | ? % 63.61/9.47 | [v3: A_n_vec_n_vec$] : (matrix_matrix_mult$(v0, v3) = all_489_0 & % 63.61/9.47 | A_n_vec_n_vec$(v3))) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 63.61/9.47 | A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ( ~ (transpose$(v0) = % 63.61/9.47 | v1) | ~ (matrix_matrix_mult$(v0, v2) = all_489_0) | ~ % 63.61/9.47 | A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v0) | ? [v3: % 63.61/9.47 | A_n_vec_n_vec$] : (matrix_matrix_mult$(v3, v1) = all_489_0 & % 63.61/9.47 | A_n_vec_n_vec$(v3))) % 63.61/9.47 | % 63.61/9.47 | ALPHA: (117) implies: % 63.61/9.47 | (118) mat$(one$) = all_489_0 % 63.61/9.47 | % 63.61/9.47 | DELTA: instantiating (38) with fresh symbol all_492_0 gives: % 63.87/9.47 | (119) mat$(one$) = all_492_0 & A_n_vec_n_vec$(all_492_0) & ! [v0: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_n_vec$] : (v1 % 63.87/9.47 | = zero$c | ~ (matrix_vector_mult$(v0, v1) = zero$c) | ~ % 63.87/9.47 | (matrix_matrix_mult$(v2, v0) = all_492_0) | ~ A_n_vec$(v1) | ~ % 63.87/9.47 | A_n_vec_n_vec$(v2) | ~ A_n_vec_n_vec$(v0)) & ? [v0: % 63.87/9.47 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v0) | ? [v1: A_n_vec_n_vec$] % 63.87/9.47 | : ? [v2: int] : ? [v3: A_n_vec$] : ? [v4: A_n_vec$] : % 63.87/9.47 | (A_n_vec$(v3) & A_n_vec_n_vec$(v1) & ((v4 = zero$c & ~ (v3 = % 63.87/9.47 | zero$c) & matrix_vector_mult$(v0, v3) = zero$c) | (v2 = % 63.87/9.47 | all_492_0 & matrix_matrix_mult$(v1, v0) = all_492_0)))) % 63.87/9.47 | % 63.87/9.47 | ALPHA: (119) implies: % 63.87/9.47 | (120) mat$(one$) = all_492_0 % 63.87/9.47 | % 63.87/9.47 | DELTA: instantiating (26) with fresh symbol all_495_0 gives: % 63.87/9.47 | (121) mat$(one$) = all_495_0 & A_n_vec_n_vec$(all_495_0) & ! [v0: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ (transpose$(v0) = % 63.87/9.47 | v1) | ~ A_n_vec_n_vec$(v0) | ~ fun_app$(orthogonal_matrix$, v0) % 63.87/9.47 | | (matrix_matrix_mult$(v1, v0) = all_495_0 & % 63.87/9.47 | matrix_matrix_mult$(v0, v1) = all_495_0)) & ! [v0: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ (transpose$(v0) = % 63.87/9.47 | v1) | ~ A_n_vec_n_vec$(v0) | fun_app$(orthogonal_matrix$, v0) | % 63.87/9.47 | ? [v2: any] : ? [v3: any] : (( ~ (v3 = all_495_0) & % 63.87/9.47 | matrix_matrix_mult$(v0, v1) = v3 & A_n_vec_n_vec$(v3)) | ( ~ % 63.87/9.47 | (v2 = all_495_0) & matrix_matrix_mult$(v1, v0) = v2 & % 63.87/9.47 | A_n_vec_n_vec$(v2)))) % 63.87/9.47 | % 63.87/9.47 | ALPHA: (121) implies: % 63.87/9.47 | (122) mat$(one$) = all_495_0 % 63.87/9.47 | % 63.87/9.47 | DELTA: instantiating (23) with fresh symbol all_498_0 gives: % 63.87/9.47 | (123) mat$(one$) = all_498_0 & A_n_vec_n_vec$(all_498_0) & ! [v0: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v1: N$] : ! [v2: A$] : ! [v3: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.87/9.47 | (mult_column$(all_498_0, v1, v2) = v3) | ~ % 63.87/9.47 | (matrix_matrix_mult$(v0, v3) = v4) | ~ A$(v2) | ~ N$(v1) | ~ % 63.87/9.47 | A_n_vec_n_vec$(v0) | (mult_column$(v0, v1, v2) = v4 & % 63.87/9.47 | A_n_vec_n_vec$(v4))) & ! [v0: A_n_vec_n_vec$] : ! [v1: N$] : ! % 63.87/9.47 | [v2: A$] : ! [v3: A_n_vec_n_vec$] : ( ~ (mult_column$(v0, v1, v2) = % 63.87/9.47 | v3) | ~ A$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v0) | ? [v4: % 63.87/9.47 | A_n_vec_n_vec$] : (mult_column$(all_498_0, v1, v2) = v4 & % 63.87/9.47 | matrix_matrix_mult$(v0, v4) = v3 & A_n_vec_n_vec$(v4) & % 63.87/9.47 | A_n_vec_n_vec$(v3))) % 63.87/9.47 | % 63.87/9.47 | ALPHA: (123) implies: % 63.87/9.47 | (124) mat$(one$) = all_498_0 % 63.87/9.47 | % 63.87/9.47 | DELTA: instantiating (30) with fresh symbol all_501_0 gives: % 63.87/9.47 | (125) mat$(one$) = all_501_0 & A_n_vec_n_vec$(all_501_0) & ! [v0: N$] : ! % 63.87/9.47 | [v1: A$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : ! % 63.87/9.47 | [v4: A_n_vec_n_vec$] : ( ~ (mult_row$(all_501_0, v0, v1) = v3) | ~ % 63.87/9.47 | (matrix_matrix_mult$(v3, v2) = v4) | ~ A$(v1) | ~ N$(v0) | ~ % 63.87/9.47 | A_n_vec_n_vec$(v2) | (mult_row$(v2, v0, v1) = v4 & % 63.87/9.47 | A_n_vec_n_vec$(v4))) & ! [v0: N$] : ! [v1: A$] : ! [v2: % 63.87/9.47 | A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : ( ~ (mult_row$(v2, v0, % 63.87/9.47 | v1) = v3) | ~ A$(v1) | ~ N$(v0) | ~ A_n_vec_n_vec$(v2) | ? % 63.87/9.47 | [v4: A_n_vec_n_vec$] : (mult_row$(all_501_0, v0, v1) = v4 & % 63.87/9.47 | matrix_matrix_mult$(v4, v2) = v3 & A_n_vec_n_vec$(v4) & % 63.87/9.47 | A_n_vec_n_vec$(v3))) % 63.87/9.47 | % 63.87/9.47 | ALPHA: (125) implies: % 63.87/9.47 | (126) mat$(one$) = all_501_0 % 63.87/9.47 | % 63.87/9.47 | DELTA: instantiating (27) with fresh symbol all_504_0 gives: % 63.87/9.48 | (127) mat$(one$) = all_504_0 & A_n_vec_n_vec$(all_504_0) & ! [v0: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v1: N$] : ! [v2: N$] : ! [v3: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (interchange_columns$(all_504_0, v1, v2) = v3) | ~ % 63.87/9.48 | (matrix_matrix_mult$(v0, v3) = v4) | ~ N$(v2) | ~ N$(v1) | ~ % 63.87/9.48 | A_n_vec_n_vec$(v0) | (interchange_columns$(v0, v1, v2) = v4 & % 63.87/9.48 | A_n_vec_n_vec$(v4))) & ! [v0: A_n_vec_n_vec$] : ! [v1: N$] : ! % 63.87/9.48 | [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ (interchange_columns$(v0, % 63.87/9.48 | v1, v2) = v3) | ~ N$(v2) | ~ N$(v1) | ~ A_n_vec_n_vec$(v0) | % 63.87/9.48 | ? [v4: A_n_vec_n_vec$] : (interchange_columns$(all_504_0, v1, v2) % 63.87/9.48 | = v4 & matrix_matrix_mult$(v0, v4) = v3 & A_n_vec_n_vec$(v4) & % 63.87/9.48 | A_n_vec_n_vec$(v3))) % 63.87/9.48 | % 63.87/9.48 | ALPHA: (127) implies: % 63.87/9.48 | (128) mat$(one$) = all_504_0 % 63.87/9.48 | % 63.87/9.48 | DELTA: instantiating (8) with fresh symbol all_507_0 gives: % 63.87/9.48 | (129) mat$(one$) = all_507_0 & A_n_vec_n_vec$(all_507_0) & ! [v0: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (matrix_matrix_mult$(v1, v0) = all_507_0) | ~ A_n_vec_n_vec$(v1) | % 63.87/9.48 | ~ A_n_vec_n_vec$(v0) | ? [v2: any] : ? [v3: A_n_vec_n_vec$] : % 63.87/9.48 | ((v3 = v1 & matrix_inv$(v0) = v1) | ( ~ (v2 = all_507_0) & % 63.87/9.48 | matrix_matrix_mult$(v0, v1) = v2 & A_n_vec_n_vec$(v2)))) & ! % 63.87/9.48 | [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (matrix_matrix_mult$(v0, v1) = all_507_0) | ~ A_n_vec_n_vec$(v1) | % 63.87/9.48 | ~ A_n_vec_n_vec$(v0) | ? [v2: any] : ? [v3: A_n_vec_n_vec$] : % 63.87/9.48 | ((v3 = v1 & matrix_inv$(v0) = v1) | ( ~ (v2 = all_507_0) & % 63.87/9.48 | matrix_matrix_mult$(v1, v0) = v2 & A_n_vec_n_vec$(v2)))) % 63.87/9.48 | % 63.87/9.48 | ALPHA: (129) implies: % 63.87/9.48 | (130) mat$(one$) = all_507_0 % 63.87/9.48 | % 63.87/9.48 | DELTA: instantiating (35) with fresh symbol all_510_0 gives: % 63.87/9.48 | (131) mat$(one$) = all_510_0 & A_n_vec_n_vec$(all_510_0) & ! [v0: N$] : ! % 63.87/9.48 | [v1: N$] : ! [v2: A$] : ! [v3: A_n_vec_n_vec$] : ! [v4: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (row_add$(all_510_0, v0, v1, v2) = v4) | ~ % 63.87/9.48 | (matrix_matrix_mult$(v4, v3) = v5) | ~ A$(v2) | ~ N$(v1) | ~ % 63.87/9.48 | N$(v0) | ~ A_n_vec_n_vec$(v3) | (row_add$(v3, v0, v1, v2) = v5 & % 63.87/9.48 | A_n_vec_n_vec$(v5))) & ! [v0: N$] : ! [v1: N$] : ! [v2: A$] : % 63.87/9.48 | ! [v3: A_n_vec_n_vec$] : ! [v4: A_n_vec_n_vec$] : ( ~ (row_add$(v3, % 63.87/9.48 | v0, v1, v2) = v4) | ~ A$(v2) | ~ N$(v1) | ~ N$(v0) | ~ % 63.87/9.48 | A_n_vec_n_vec$(v3) | ? [v5: A_n_vec_n_vec$] : (row_add$(all_510_0, % 63.87/9.48 | v0, v1, v2) = v5 & matrix_matrix_mult$(v5, v3) = v4 & % 63.87/9.48 | A_n_vec_n_vec$(v5) & A_n_vec_n_vec$(v4))) % 63.87/9.48 | % 63.87/9.48 | ALPHA: (131) implies: % 63.87/9.48 | (132) mat$(one$) = all_510_0 % 63.87/9.48 | % 63.87/9.48 | DELTA: instantiating (21) with fresh symbol all_513_0 gives: % 63.87/9.48 | (133) mat$(one$) = all_513_0 & A_n_vec_n_vec$(all_513_0) & ! [v0: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v1: N$] : ! [v2: N$] : ! [v3: A$] : ! [v4: % 63.87/9.48 | A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (column_add$(all_513_0, v1, v2, v3) = v4) | ~ % 63.87/9.48 | (matrix_matrix_mult$(v0, v4) = v5) | ~ A$(v3) | ~ N$(v2) | ~ % 63.87/9.48 | N$(v1) | ~ A_n_vec_n_vec$(v0) | (column_add$(v0, v1, v2, v3) = v5 % 63.87/9.48 | & A_n_vec_n_vec$(v5))) & ! [v0: A_n_vec_n_vec$] : ! [v1: N$] : % 63.87/9.48 | ! [v2: N$] : ! [v3: A$] : ! [v4: A_n_vec_n_vec$] : ( ~ % 63.87/9.48 | (column_add$(v0, v1, v2, v3) = v4) | ~ A$(v3) | ~ N$(v2) | ~ % 63.87/9.48 | N$(v1) | ~ A_n_vec_n_vec$(v0) | ? [v5: A_n_vec_n_vec$] : % 63.87/9.48 | (column_add$(all_513_0, v1, v2, v3) = v5 & matrix_matrix_mult$(v0, % 63.87/9.48 | v5) = v4 & A_n_vec_n_vec$(v5) & A_n_vec_n_vec$(v4))) % 63.87/9.48 | % 63.87/9.48 | ALPHA: (133) implies: % 63.87/9.48 | (134) mat$(one$) = all_513_0 % 64.02/9.48 | % 64.02/9.48 | DELTA: instantiating (36) with fresh symbol all_516_0 gives: % 64.02/9.48 | (135) mat$(one$) = all_516_0 & A_n_vec_n_vec$(all_516_0) & ! [v0: A$] : ! % 64.02/9.48 | [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ (times$(v1, % 64.02/9.48 | v0) = one$) | ~ (mult_row$(all_516_0, v2, v0) = v3) | ~ % 64.02/9.48 | A$(v1) | ~ A$(v0) | ~ N$(v2) | fun_app$(invertible$, v3) | ? % 64.02/9.48 | [v4: A$] : ( ~ (v4 = one$) & times$(v0, v1) = v4 & A$(v4))) & ! % 64.02/9.48 | [v0: A$] : ! [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ % 64.02/9.48 | (times$(v0, v1) = one$) | ~ (mult_row$(all_516_0, v2, v0) = v3) | % 64.02/9.48 | ~ A$(v1) | ~ A$(v0) | ~ N$(v2) | fun_app$(invertible$, v3) | ? % 64.02/9.48 | [v4: A$] : ( ~ (v4 = one$) & times$(v1, v0) = v4 & A$(v4))) % 64.02/9.48 | % 64.02/9.48 | ALPHA: (135) implies: % 64.02/9.48 | (136) mat$(one$) = all_516_0 % 64.02/9.48 | % 64.02/9.48 | DELTA: instantiating (31) with fresh symbol all_519_0 gives: % 64.02/9.48 | (137) mat$(one$) = all_519_0 & A_n_vec_n_vec$(all_519_0) & ! [v0: A$] : ! % 64.02/9.48 | [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ (times$(v1, % 64.02/9.48 | v0) = one$) | ~ (mult_column$(all_519_0, v2, v0) = v3) | ~ % 64.02/9.48 | A$(v1) | ~ A$(v0) | ~ N$(v2) | fun_app$(invertible$, v3) | ? % 64.02/9.48 | [v4: A$] : ( ~ (v4 = one$) & times$(v0, v1) = v4 & A$(v4))) & ! % 64.02/9.48 | [v0: A$] : ! [v1: A$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ( ~ % 64.02/9.48 | (times$(v0, v1) = one$) | ~ (mult_column$(all_519_0, v2, v0) = v3) % 64.02/9.48 | | ~ A$(v1) | ~ A$(v0) | ~ N$(v2) | fun_app$(invertible$, v3) | % 64.02/9.48 | ? [v4: A$] : ( ~ (v4 = one$) & times$(v1, v0) = v4 & A$(v4))) % 64.02/9.48 | % 64.02/9.48 | ALPHA: (137) implies: % 64.02/9.48 | (138) mat$(one$) = all_519_0 % 64.02/9.48 | % 64.02/9.48 | DELTA: instantiating (14) with fresh symbol all_522_0 gives: % 64.02/9.48 | (139) mat$(one$) = all_522_0 & A_n_vec_n_vec$(all_522_0) & ! [v0: % 64.02/9.48 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 64.02/9.48 | (matrix_matrix_mult$(v1, v0) = all_522_0) | ~ A_n_vec_n_vec$(v1) | % 64.02/9.48 | ~ A_n_vec_n_vec$(v0) | fun_app$(invertible$, v0) | ? [v2: any] : % 64.02/9.48 | ( ~ (v2 = all_522_0) & matrix_matrix_mult$(v0, v1) = v2 & % 64.02/9.48 | A_n_vec_n_vec$(v2))) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 64.02/9.48 | A_n_vec_n_vec$] : ( ~ (matrix_matrix_mult$(v0, v1) = all_522_0) | % 64.02/9.48 | ~ A_n_vec_n_vec$(v1) | ~ A_n_vec_n_vec$(v0) | % 64.02/9.48 | fun_app$(invertible$, v0) | ? [v2: any] : ( ~ (v2 = all_522_0) & % 64.02/9.48 | matrix_matrix_mult$(v1, v0) = v2 & A_n_vec_n_vec$(v2))) & ! [v0: % 64.02/9.48 | A_n_vec_n_vec$] : ( ~ A_n_vec_n_vec$(v0) | ~ fun_app$(invertible$, % 64.02/9.48 | v0) | ? [v1: A_n_vec_n_vec$] : (matrix_matrix_mult$(v1, v0) = % 64.02/9.48 | all_522_0 & matrix_matrix_mult$(v0, v1) = all_522_0 & % 64.02/9.48 | A_n_vec_n_vec$(v1))) % 64.02/9.48 | % 64.02/9.48 | ALPHA: (139) implies: % 64.02/9.48 | (140) mat$(one$) = all_522_0 % 64.02/9.48 | % 64.02/9.48 | DELTA: instantiating (33) with fresh symbol all_525_0 gives: % 64.02/9.49 | (141) mat$(one$) = all_525_0 & A_n_vec_n_vec$(all_525_0) & ! [v0: N$] : ! % 64.02/9.49 | [v1: N$] : ! [v2: A_n_vec_n_vec$] : ! [v3: N_a_n_vec_n_vec_fun$] : % 64.02/9.49 | ! [v4: A_n_vec_n_vec$] : ! [v5: A_n_vec_n_vec$] : ( ~ % 64.02/9.49 | (interchange_rows$(all_525_0, v0) = v3) | ~ (fun_app$c(v3, v1) = % 64.02/9.49 | v4) | ~ (matrix_matrix_mult$(v4, v2) = v5) | ~ N$(v1) | ~ % 64.02/9.49 | N$(v0) | ~ A_n_vec_n_vec$(v2) | ? [v6: N_a_n_vec_n_vec_fun$] : % 64.02/9.49 | (interchange_rows$(v2, v0) = v6 & fun_app$c(v6, v1) = v5 & % 64.02/9.49 | N_a_n_vec_n_vec_fun$(v6) & A_n_vec_n_vec$(v5))) & ! [v0: N$] : % 64.02/9.49 | ! [v1: N$] : ! [v2: A_n_vec_n_vec$] : ! [v3: N_a_n_vec_n_vec_fun$] % 64.02/9.49 | : ! [v4: A_n_vec_n_vec$] : ( ~ (interchange_rows$(v2, v0) = v3) | ~ % 64.02/9.49 | (fun_app$c(v3, v1) = v4) | ~ N$(v1) | ~ N$(v0) | ~ % 64.02/9.49 | A_n_vec_n_vec$(v2) | ? [v5: N_a_n_vec_n_vec_fun$] : ? [v6: % 64.02/9.49 | A_n_vec_n_vec$] : (interchange_rows$(all_525_0, v0) = v5 & % 64.02/9.49 | fun_app$c(v5, v1) = v6 & matrix_matrix_mult$(v6, v2) = v4 & % 64.02/9.49 | N_a_n_vec_n_vec_fun$(v5) & A_n_vec_n_vec$(v6) & % 64.02/9.49 | A_n_vec_n_vec$(v4))) % 64.02/9.49 | % 64.02/9.49 | ALPHA: (141) implies: % 64.02/9.49 | (142) mat$(one$) = all_525_0 % 64.02/9.49 | % 64.02/9.49 | DELTA: instantiating (9) with fresh symbol all_528_0 gives: % 64.02/9.49 | (143) mat$(one$) = all_528_0 & A_n_vec_n_vec$(all_528_0) & ! [v0: % 64.02/9.49 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: int] : (v2 = % 64.02/9.49 | all_528_0 | ~ (matrix_matrix_mult$(v1, v0) = v2) | ~ % 64.02/9.49 | A_n_vec_n_vec$(v1) | ~ A_n_vec_n_vec$(v0) | ? [v3: any] : ( ~ (v3 % 64.02/9.49 | = all_528_0) & matrix_matrix_mult$(v0, v1) = v3 & % 64.02/9.49 | A_n_vec_n_vec$(v3))) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 64.02/9.49 | A_n_vec_n_vec$] : ! [v2: int] : (v2 = all_528_0 | ~ % 64.02/9.49 | (matrix_matrix_mult$(v0, v1) = v2) | ~ A_n_vec_n_vec$(v1) | ~ % 64.02/9.49 | A_n_vec_n_vec$(v0) | ? [v3: any] : ( ~ (v3 = all_528_0) & % 64.02/9.49 | matrix_matrix_mult$(v1, v0) = v3 & A_n_vec_n_vec$(v3))) & ! [v0: % 64.02/9.49 | A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 64.02/9.49 | (matrix_matrix_mult$(v1, v0) = all_528_0) | ~ A_n_vec_n_vec$(v1) | % 64.02/9.49 | ~ A_n_vec_n_vec$(v0) | matrix_matrix_mult$(v0, v1) = all_528_0) & % 64.02/9.49 | ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ( ~ % 64.02/9.49 | (matrix_matrix_mult$(v0, v1) = all_528_0) | ~ A_n_vec_n_vec$(v1) | % 64.02/9.49 | ~ A_n_vec_n_vec$(v0) | matrix_matrix_mult$(v1, v0) = all_528_0) % 64.02/9.49 | % 64.02/9.49 | ALPHA: (143) implies: % 64.02/9.49 | (144) mat$(one$) = all_528_0 % 64.02/9.49 | % 64.02/9.49 | GROUND_INST: instantiating (44) with all_464_2, all_470_0, a$, p$, simplifying % 64.02/9.49 | with (95), (106) gives: % 64.02/9.49 | (145) all_470_0 = all_464_2 % 64.02/9.49 | % 64.02/9.49 | GROUND_INST: instantiating (44) with all_402_0, all_470_0, a$, p$, simplifying % 64.02/9.49 | with (54), (106) gives: % 64.02/9.49 | (146) all_470_0 = all_402_0 % 64.02/9.49 | % 64.02/9.49 | GROUND_INST: instantiating (44) with all_467_0, all_470_2, p$, all_467_1, % 64.02/9.49 | simplifying with (101) gives: % 64.02/9.49 | (147) all_470_2 = all_467_0 | ~ (matrix_matrix_mult$(all_467_1, p$) = % 64.02/9.49 | all_470_2) % 64.02/9.49 | % 64.02/9.49 | GROUND_INST: instantiating (44) with all_467_2, all_470_1, a$, all_467_0, % 64.02/9.49 | simplifying with (102) gives: % 64.02/9.49 | (148) all_470_1 = all_467_2 | ~ (matrix_matrix_mult$(all_467_0, a$) = % 64.02/9.49 | all_470_1) % 64.02/9.49 | % 64.02/9.49 | GROUND_INST: instantiating (44) with a$, all_470_1, a$, all_398_0, simplifying % 64.02/9.49 | with (48) gives: % 64.06/9.49 | (149) all_470_1 = a$ | ~ (matrix_matrix_mult$(all_398_0, a$) = all_470_1) % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (41) with all_447_2, all_464_3, p$, simplifying % 64.06/9.49 | with (82), (97) gives: % 64.06/9.49 | (150) all_464_3 = all_447_2 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (41) with all_464_3, all_467_1, p$, simplifying % 64.06/9.49 | with (97), (103) gives: % 64.06/9.49 | (151) all_467_1 = all_464_3 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (41) with all_467_1, all_470_3, p$, simplifying % 64.06/9.49 | with (103), (110) gives: % 64.06/9.49 | (152) all_470_3 = all_467_1 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (41) with all_413_1, all_470_3, p$, simplifying % 64.06/9.49 | with (59), (110) gives: % 64.06/9.49 | (153) all_470_3 = all_413_1 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_398_0, all_400_0, one$, simplifying % 64.06/9.49 | with (49), (51) gives: % 64.06/9.49 | (154) all_400_0 = all_398_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_404_0, all_426_0, one$, simplifying % 64.06/9.49 | with (57), (67) gives: % 64.06/9.49 | (155) all_426_0 = all_404_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_400_0, all_426_0, one$, simplifying % 64.06/9.49 | with (51), (67) gives: % 64.06/9.49 | (156) all_426_0 = all_400_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_426_0, all_429_0, one$, simplifying % 64.06/9.49 | with (67), (69) gives: % 64.06/9.49 | (157) all_429_0 = all_426_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_452_0, all_455_0, one$, simplifying % 64.06/9.49 | with (87), (89) gives: % 64.06/9.49 | (158) all_455_0 = all_452_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_464_0, all_472_0, one$, simplifying % 64.06/9.49 | with (98), (112) gives: % 64.06/9.49 | (159) all_472_0 = all_464_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_472_0, all_475_0, one$, simplifying % 64.06/9.49 | with (112), (114) gives: % 64.06/9.49 | (160) all_475_0 = all_472_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_455_0, all_486_0, one$, simplifying % 64.06/9.49 | with (89), (116) gives: % 64.06/9.49 | (161) all_486_0 = all_455_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_486_0, all_489_0, one$, simplifying % 64.06/9.49 | with (116), (118) gives: % 64.06/9.49 | (162) all_489_0 = all_486_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_489_0, all_492_0, one$, simplifying % 64.06/9.49 | with (118), (120) gives: % 64.06/9.49 | (163) all_492_0 = all_489_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_461_0, all_492_0, one$, simplifying % 64.06/9.49 | with (93), (120) gives: % 64.06/9.49 | (164) all_492_0 = all_461_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_452_0, all_498_0, one$, simplifying % 64.06/9.49 | with (87), (124) gives: % 64.06/9.49 | (165) all_498_0 = all_452_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_449_0, all_498_0, one$, simplifying % 64.06/9.49 | with (85), (124) gives: % 64.06/9.49 | (166) all_498_0 = all_449_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_444_0, all_498_0, one$, simplifying % 64.06/9.49 | with (77), (124) gives: % 64.06/9.49 | (167) all_498_0 = all_444_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_458_0, all_501_0, one$, simplifying % 64.06/9.49 | with (91), (126) gives: % 64.06/9.49 | (168) all_501_0 = all_458_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_396_0, all_501_0, one$, simplifying % 64.06/9.49 | with (46), (126) gives: % 64.06/9.49 | (169) all_501_0 = all_396_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_504_0, all_507_0, one$, simplifying % 64.06/9.49 | with (128), (130) gives: % 64.06/9.49 | (170) all_507_0 = all_504_0 % 64.06/9.49 | % 64.06/9.49 | GROUND_INST: instantiating (42) with all_472_0, all_507_0, one$, simplifying % 64.06/9.49 | with (112), (130) gives: % 64.06/9.49 | (171) all_507_0 = all_472_0 % 64.06/9.49 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_444_0, all_507_0, one$, simplifying % 64.06/9.50 | with (77), (130) gives: % 64.06/9.50 | (172) all_507_0 = all_444_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_495_0, all_510_0, one$, simplifying % 64.06/9.50 | with (122), (132) gives: % 64.06/9.50 | (173) all_510_0 = all_495_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_467_3, all_510_0, one$, simplifying % 64.06/9.50 | with (104), (132) gives: % 64.06/9.50 | (174) all_510_0 = all_467_3 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_458_0, all_510_0, one$, simplifying % 64.06/9.50 | with (91), (132) gives: % 64.06/9.50 | (175) all_510_0 = all_458_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_426_0, all_510_0, one$, simplifying % 64.06/9.50 | with (67), (132) gives: % 64.06/9.50 | (176) all_510_0 = all_426_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_507_0, all_513_0, one$, simplifying % 64.06/9.50 | with (130), (134) gives: % 64.06/9.50 | (177) all_513_0 = all_507_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_447_1, all_513_0, one$, simplifying % 64.06/9.50 | with (83), (134) gives: % 64.06/9.50 | (178) all_513_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_444_0, all_516_0, one$, simplifying % 64.06/9.50 | with (77), (136) gives: % 64.06/9.50 | (179) all_516_0 = all_444_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_438_0, all_516_0, one$, simplifying % 64.06/9.50 | with (73), (136) gives: % 64.06/9.50 | (180) all_516_0 = all_438_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_486_0, all_519_0, one$, simplifying % 64.06/9.50 | with (116), (138) gives: % 64.06/9.50 | (181) all_519_0 = all_486_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_441_0, all_519_0, one$, simplifying % 64.06/9.50 | with (75), (138) gives: % 64.06/9.50 | (182) all_519_0 = all_441_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_475_0, all_522_0, one$, simplifying % 64.06/9.50 | with (114), (140) gives: % 64.06/9.50 | (183) all_522_0 = all_475_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_419_0, all_522_0, one$, simplifying % 64.06/9.50 | with (64), (140) gives: % 64.06/9.50 | (184) all_522_0 = all_419_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_516_0, all_525_0, one$, simplifying % 64.06/9.50 | with (136), (142) gives: % 64.06/9.50 | (185) all_525_0 = all_516_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_435_0, all_525_0, one$, simplifying % 64.06/9.50 | with (71), (142) gives: % 64.06/9.50 | (186) all_525_0 = all_435_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_429_0, all_525_0, one$, simplifying % 64.06/9.50 | with (69), (142) gives: % 64.06/9.50 | (187) all_525_0 = all_429_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_495_0, all_528_0, one$, simplifying % 64.06/9.50 | with (122), (144) gives: % 64.06/9.50 | (188) all_528_0 = all_495_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (42) with all_413_0, all_528_0, one$, simplifying % 64.06/9.50 | with (60), (144) gives: % 64.06/9.50 | (189) all_528_0 = all_413_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (43) with all_402_0, all_417_1, a$, simplifying % 64.06/9.50 | with (55), (62) gives: % 64.06/9.50 | (190) all_417_1 = all_402_0 % 64.06/9.50 | % 64.06/9.50 | GROUND_INST: instantiating (43) with all_400_0, all_417_1, a$, simplifying % 64.06/9.50 | with (52), (62) gives: % 64.06/9.50 | (191) all_417_1 = all_400_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (188), (189) imply: % 64.06/9.50 | (192) all_495_0 = all_413_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (192) implies: % 64.06/9.50 | (193) all_495_0 = all_413_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (186), (187) imply: % 64.06/9.50 | (194) all_435_0 = all_429_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (185), (186) imply: % 64.06/9.50 | (195) all_516_0 = all_435_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (195) implies: % 64.06/9.50 | (196) all_516_0 = all_435_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (183), (184) imply: % 64.06/9.50 | (197) all_475_0 = all_419_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (197) implies: % 64.06/9.50 | (198) all_475_0 = all_419_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (181), (182) imply: % 64.06/9.50 | (199) all_486_0 = all_441_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (199) implies: % 64.06/9.50 | (200) all_486_0 = all_441_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (179), (180) imply: % 64.06/9.50 | (201) all_444_0 = all_438_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (201) implies: % 64.06/9.50 | (202) all_444_0 = all_438_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (180), (196) imply: % 64.06/9.50 | (203) all_438_0 = all_435_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (177), (178) imply: % 64.06/9.50 | (204) all_507_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | SIMP: (204) implies: % 64.06/9.50 | (205) all_507_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (173), (174) imply: % 64.06/9.50 | (206) all_495_0 = all_467_3 % 64.06/9.50 | % 64.06/9.50 | SIMP: (206) implies: % 64.06/9.50 | (207) all_495_0 = all_467_3 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (174), (175) imply: % 64.06/9.50 | (208) all_467_3 = all_458_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (174), (176) imply: % 64.06/9.50 | (209) all_467_3 = all_426_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (170), (171) imply: % 64.06/9.50 | (210) all_504_0 = all_472_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (170), (172) imply: % 64.06/9.50 | (211) all_504_0 = all_444_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (170), (205) imply: % 64.06/9.50 | (212) all_504_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (211), (212) imply: % 64.06/9.50 | (213) all_447_1 = all_444_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (210), (212) imply: % 64.06/9.50 | (214) all_472_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | SIMP: (214) implies: % 64.06/9.50 | (215) all_472_0 = all_447_1 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (168), (169) imply: % 64.06/9.50 | (216) all_458_0 = all_396_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (216) implies: % 64.06/9.50 | (217) all_458_0 = all_396_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (165), (166) imply: % 64.06/9.50 | (218) all_452_0 = all_449_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (218) implies: % 64.06/9.50 | (219) all_452_0 = all_449_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (166), (167) imply: % 64.06/9.50 | (220) all_449_0 = all_444_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (193), (207) imply: % 64.06/9.50 | (221) all_467_3 = all_413_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (221) implies: % 64.06/9.50 | (222) all_467_3 = all_413_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (163), (164) imply: % 64.06/9.50 | (223) all_489_0 = all_461_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (223) implies: % 64.06/9.50 | (224) all_489_0 = all_461_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (162), (224) imply: % 64.06/9.50 | (225) all_486_0 = all_461_0 % 64.06/9.50 | % 64.06/9.50 | SIMP: (225) implies: % 64.06/9.50 | (226) all_486_0 = all_461_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (200), (226) imply: % 64.06/9.50 | (227) all_461_0 = all_441_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (161), (226) imply: % 64.06/9.50 | (228) all_461_0 = all_455_0 % 64.06/9.50 | % 64.06/9.50 | COMBINE_EQS: (160), (198) imply: % 64.06/9.51 | (229) all_472_0 = all_419_0 % 64.06/9.51 | % 64.06/9.51 | SIMP: (229) implies: % 64.06/9.51 | (230) all_472_0 = all_419_0 % 64.06/9.51 | % 64.06/9.51 | COMBINE_EQS: (159), (215) imply: % 64.06/9.51 | (231) all_464_0 = all_447_1 % 64.06/9.51 | % 64.06/9.51 | COMBINE_EQS: (159), (230) imply: % 64.06/9.51 | (232) all_464_0 = all_419_0 % 64.06/9.51 | % 64.06/9.51 | COMBINE_EQS: (145), (146) imply: % 64.06/9.51 | (233) all_464_2 = all_402_0 % 64.06/9.51 | % 64.06/9.51 | SIMP: (233) implies: % 64.06/9.51 | (234) all_464_2 = all_402_0 % 64.06/9.51 | % 64.14/9.51 | COMBINE_EQS: (152), (153) imply: % 64.14/9.51 | (235) all_467_1 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | SIMP: (235) implies: % 64.14/9.51 | (236) all_467_1 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (151), (236) imply: % 64.14/9.51 | (237) all_464_3 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | SIMP: (237) implies: % 64.14/9.51 | (238) all_464_3 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (209), (222) imply: % 64.14/9.51 | (239) all_426_0 = all_413_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (239) implies: % 64.14/9.51 | (240) all_426_0 = all_413_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (208), (222) imply: % 64.14/9.51 | (241) all_458_0 = all_413_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (241) implies: % 64.14/9.51 | (242) all_458_0 = all_413_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (231), (232) imply: % 64.14/9.51 | (243) all_447_1 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (243) implies: % 64.14/9.51 | (244) all_447_1 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (150), (238) imply: % 64.14/9.51 | (245) all_447_2 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | SIMP: (245) implies: % 64.14/9.51 | (246) all_447_2 = all_413_1 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (227), (228) imply: % 64.14/9.51 | (247) all_455_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (247) implies: % 64.14/9.51 | (248) all_455_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (217), (242) imply: % 64.14/9.51 | (249) all_413_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (249) implies: % 64.14/9.51 | (250) all_413_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (158), (248) imply: % 64.14/9.51 | (251) all_452_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (251) implies: % 64.14/9.51 | (252) all_452_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (219), (252) imply: % 64.14/9.51 | (253) all_449_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (253) implies: % 64.14/9.51 | (254) all_449_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (220), (254) imply: % 64.14/9.51 | (255) all_444_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (255) implies: % 64.14/9.51 | (256) all_444_0 = all_441_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (213), (244) imply: % 64.14/9.51 | (257) all_444_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (257) implies: % 64.14/9.51 | (258) all_444_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (202), (256) imply: % 64.14/9.51 | (259) all_441_0 = all_438_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (256), (258) imply: % 64.14/9.51 | (260) all_441_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (259), (260) imply: % 64.14/9.51 | (261) all_438_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (261) implies: % 64.14/9.51 | (262) all_438_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (203), (262) imply: % 64.14/9.51 | (263) all_435_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (263) implies: % 64.14/9.51 | (264) all_435_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (194), (264) imply: % 64.14/9.51 | (265) all_429_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (265) implies: % 64.14/9.51 | (266) all_429_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (157), (266) imply: % 64.14/9.51 | (267) all_426_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (267) implies: % 64.14/9.51 | (268) all_426_0 = all_419_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (156), (268) imply: % 64.14/9.51 | (269) all_419_0 = all_400_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (155), (268) imply: % 64.14/9.51 | (270) all_419_0 = all_404_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (240), (268) imply: % 64.14/9.51 | (271) all_419_0 = all_413_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (269), (270) imply: % 64.14/9.51 | (272) all_404_0 = all_400_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (270), (271) imply: % 64.14/9.51 | (273) all_413_0 = all_404_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (273) implies: % 64.14/9.51 | (274) all_413_0 = all_404_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (190), (191) imply: % 64.14/9.51 | (275) all_402_0 = all_400_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (250), (274) imply: % 64.14/9.51 | (276) all_404_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (276) implies: % 64.14/9.51 | (277) all_404_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (272), (277) imply: % 64.14/9.51 | (278) all_400_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (278) implies: % 64.14/9.51 | (279) all_400_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (154), (279) imply: % 64.14/9.51 | (280) all_398_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | SIMP: (280) implies: % 64.14/9.51 | (281) all_398_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (275), (279) imply: % 64.14/9.51 | (282) all_402_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (270), (277) imply: % 64.14/9.51 | (283) all_419_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (244), (283) imply: % 64.14/9.51 | (284) all_447_1 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (234), (282) imply: % 64.14/9.51 | (285) all_464_2 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (222), (250) imply: % 64.14/9.51 | (286) all_467_3 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | COMBINE_EQS: (146), (282) imply: % 64.14/9.51 | (287) all_470_0 = all_396_0 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (79), (246) imply: % 64.14/9.51 | (288) ~ (all_447_0 = all_413_1) % 64.14/9.51 | % 64.14/9.51 | REDUCE: (108), (153), (287) imply: % 64.14/9.51 | (289) matrix_matrix_mult$(all_413_1, all_396_0) = all_470_1 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (107), (153) imply: % 64.14/9.51 | (290) matrix_matrix_mult$(all_413_1, p$) = all_470_2 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (100), (286) imply: % 64.14/9.51 | (291) matrix_matrix_mult$(all_396_0, a$) = all_467_2 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (96), (238), (285) imply: % 64.14/9.51 | (292) matrix_matrix_mult$(all_413_1, all_396_0) = all_464_1 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (81), (246), (284) imply: % 64.14/9.51 | (293) matrix_matrix_mult$(all_413_1, all_396_0) = all_447_0 % 64.14/9.51 | % 64.14/9.51 | REDUCE: (80), (246) imply: % 64.14/9.51 | (294) A_n_vec_n_vec$(all_413_1) % 64.14/9.51 | % 64.14/9.51 | BETA: splitting (147) gives: % 64.14/9.51 | % 64.18/9.51 | Case 1: % 64.18/9.51 | | % 64.18/9.51 | | (295) ~ (matrix_matrix_mult$(all_467_1, p$) = all_470_2) % 64.18/9.52 | | % 64.18/9.52 | | REDUCE: (236), (295) imply: % 64.18/9.52 | | (296) ~ (matrix_matrix_mult$(all_413_1, p$) = all_470_2) % 64.18/9.52 | | % 64.18/9.52 | | PRED_UNIFY: (290), (296) imply: % 64.18/9.52 | | (297) $false % 64.18/9.52 | | % 64.18/9.52 | | CLOSE: (297) is inconsistent. % 64.18/9.52 | | % 64.18/9.52 | Case 2: % 64.18/9.52 | | % 64.18/9.52 | | (298) all_470_2 = all_467_0 % 64.18/9.52 | | % 64.18/9.52 | | REDUCE: (109), (298) imply: % 64.18/9.52 | | (299) matrix_matrix_mult$(all_467_0, a$) = all_470_1 % 64.18/9.52 | | % 64.18/9.52 | | BETA: splitting (148) gives: % 64.18/9.52 | | % 64.18/9.52 | | Case 1: % 64.18/9.52 | | | % 64.18/9.52 | | | (300) ~ (matrix_matrix_mult$(all_467_0, a$) = all_470_1) % 64.18/9.52 | | | % 64.18/9.52 | | | PRED_UNIFY: (299), (300) imply: % 64.18/9.52 | | | (301) $false % 64.18/9.52 | | | % 64.18/9.52 | | | CLOSE: (301) is inconsistent. % 64.18/9.52 | | | % 64.18/9.52 | | Case 2: % 64.18/9.52 | | | % 64.18/9.52 | | | (302) all_470_1 = all_467_2 % 64.18/9.52 | | | % 64.18/9.52 | | | REDUCE: (289), (302) imply: % 64.18/9.52 | | | (303) matrix_matrix_mult$(all_413_1, all_396_0) = all_467_2 % 64.18/9.52 | | | % 64.18/9.52 | | | BETA: splitting (149) gives: % 64.18/9.52 | | | % 64.18/9.52 | | | Case 1: % 64.18/9.52 | | | | % 64.18/9.52 | | | | (304) ~ (matrix_matrix_mult$(all_398_0, a$) = all_470_1) % 64.18/9.52 | | | | % 64.18/9.52 | | | | REDUCE: (281), (302), (304) imply: % 64.18/9.52 | | | | (305) ~ (matrix_matrix_mult$(all_396_0, a$) = all_467_2) % 64.18/9.52 | | | | % 64.18/9.52 | | | | PRED_UNIFY: (291), (305) imply: % 64.18/9.52 | | | | (306) $false % 64.18/9.52 | | | | % 64.18/9.52 | | | | CLOSE: (306) is inconsistent. % 64.18/9.52 | | | | % 64.18/9.52 | | | Case 2: % 64.18/9.52 | | | | % 64.18/9.52 | | | | (307) all_470_1 = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | COMBINE_EQS: (302), (307) imply: % 64.18/9.52 | | | | (308) all_467_2 = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | REDUCE: (303), (308) imply: % 64.18/9.52 | | | | (309) matrix_matrix_mult$(all_413_1, all_396_0) = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | GROUND_INST: instantiating (44) with all_447_0, all_464_1, all_396_0, % 64.18/9.52 | | | | all_413_1, simplifying with (292), (293) gives: % 64.18/9.52 | | | | (310) all_464_1 = all_447_0 % 64.18/9.52 | | | | % 64.18/9.52 | | | | GROUND_INST: instantiating (44) with a$, all_464_1, all_396_0, % 64.18/9.52 | | | | all_413_1, simplifying with (292), (309) gives: % 64.18/9.52 | | | | (311) all_464_1 = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | COMBINE_EQS: (310), (311) imply: % 64.18/9.52 | | | | (312) all_447_0 = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | SIMP: (312) implies: % 64.18/9.52 | | | | (313) all_447_0 = a$ % 64.18/9.52 | | | | % 64.18/9.52 | | | | REDUCE: (288), (313) imply: % 64.18/9.52 | | | | (314) ~ (all_413_1 = a$) % 64.18/9.52 | | | | % 64.18/9.52 | | | | SIMP: (314) implies: % 64.18/9.52 | | | | (315) ~ (all_413_1 = a$) % 64.18/9.52 | | | | % 64.18/9.52 | | | | GROUND_INST: instantiating (65) with all_413_1, a$, simplifying with % 64.18/9.52 | | | | (294) gives: % 64.18/9.52 | | | | (316) all_413_1 = a$ | ~ (matrix_matrix_mult$(all_413_1, all_419_0) % 64.18/9.52 | | | | = a$) % 64.18/9.52 | | | | % 64.18/9.52 | | | | BETA: splitting (316) gives: % 64.18/9.52 | | | | % 64.18/9.52 | | | | Case 1: % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | (317) ~ (matrix_matrix_mult$(all_413_1, all_419_0) = a$) % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | REDUCE: (283), (317) imply: % 64.18/9.52 | | | | | (318) ~ (matrix_matrix_mult$(all_413_1, all_396_0) = a$) % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | PRED_UNIFY: (309), (318) imply: % 64.18/9.52 | | | | | (319) $false % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | CLOSE: (319) is inconsistent. % 64.18/9.52 | | | | | % 64.18/9.52 | | | | Case 2: % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | (320) all_413_1 = a$ % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | REDUCE: (315), (320) imply: % 64.18/9.52 | | | | | (321) $false % 64.18/9.52 | | | | | % 64.18/9.52 | | | | | CLOSE: (321) is inconsistent. % 64.18/9.52 | | | | | % 64.18/9.52 | | | | End of split % 64.18/9.52 | | | | % 64.18/9.52 | | | End of split % 64.18/9.52 | | | % 64.18/9.52 | | End of split % 64.18/9.52 | | % 64.18/9.52 | End of split % 64.18/9.52 | % 64.18/9.52 End of proof % 64.18/9.52 % SZS output end Proof for theBenchmark % 64.18/9.52 % 64.18/9.52 8884ms %------------------------------------------------------------------------------