%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : RNG081+2 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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 : Sat Jun 21 05:24:08 AM UTC 2025
% Result : Theorem 0.12s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : RNG081+2 : TPTP v9.0.0. Released v4.0.0.
% 0.08/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 03:19:42 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.40 % SZS status Theorem
% 0.12/0.40 % SZS output start Proof
% 0.12/0.40 tff(sdtlseqdt0_type, type, (
% 0.12/0.40 sdtlseqdt0: ( $i * $i ) > $o)).
% 0.12/0.40 tff(sdtasdt0_type, type, (
% 0.12/0.40 sdtasdt0: ( $i * $i ) > $i)).
% 0.12/0.40 tff(sdtasasdt0_type, type, (
% 0.12/0.40 sdtasasdt0: ( $i * $i ) > $i)).
% 0.12/0.40 tff(xt_type, type, (
% 0.12/0.40 xt: $i)).
% 0.12/0.40 tff(xs_type, type, (
% 0.12/0.40 xs: $i)).
% 0.12/0.40 tff(sz0z00_type, type, (
% 0.12/0.40 sz0z00: $i)).
% 0.12/0.40 tff(smndt0_type, type, (
% 0.12/0.40 smndt0: $i > $i)).
% 0.12/0.40 tff(sdtpldt0_type, type, (
% 0.12/0.40 sdtpldt0: ( $i * $i ) > $i)).
% 0.12/0.40 tff(aScalar0_type, type, (
% 0.12/0.40 aScalar0: $i > $o)).
% 0.12/0.40 tff(sz00_type, type, (
% 0.12/0.40 sz00: $i)).
% 0.12/0.40 tff(aDimensionOf0_type, type, (
% 0.12/0.40 aDimensionOf0: $i > $i)).
% 0.12/0.40 tff(sdtlbdtrb0_type, type, (
% 0.12/0.40 sdtlbdtrb0: ( $i * $i ) > $i)).
% 0.12/0.40 tff(sziznziztdt0_type, type, (
% 0.12/0.40 sziznziztdt0: $i > $i)).
% 0.12/0.40 tff(aNaturalNumber0_type, type, (
% 0.12/0.40 aNaturalNumber0: $i > $o)).
% 0.12/0.40 tff(szszuzczcdt0_type, type, (
% 0.12/0.40 szszuzczcdt0: $i > $i)).
% 0.12/0.40 tff(aVector0_type, type, (
% 0.12/0.40 aVector0: $i > $o)).
% 0.12/0.40 tff(1,plain,
% 0.12/0.40 (^[W0: $i] : refl(((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00))))) <=> ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00))))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(2,plain,
% 0.12/0.40 (![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00))))) <=> ![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[1])).
% 0.12/0.40 tff(3,plain,
% 0.12/0.40 (^[W0: $i] : rewrite(((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))) <=> ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00))))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(4,plain,
% 0.12/0.40 (![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))) <=> ![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[3])).
% 0.12/0.40 tff(5,plain,
% 0.12/0.40 (![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))) <=> ![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(6,plain,
% 0.12/0.40 (^[W0: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00))), (((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) <=> (((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)))), rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00))), (((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00)))), ((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) <=> (((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)))), rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00))), ((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)))), (((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) <=> (((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)))), rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00))), (((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00)))), ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) <=> (((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)))), rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0))), ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0)))), (((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00)) <=> (((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00)))), rewrite((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))), (((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00)) <=> ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))), ((aScalar0(W0) => ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00))) <=> (aScalar0(W0) => ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))))), rewrite((aScalar0(W0) => ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00))) <=> ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))), ((aScalar0(W0) => ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00))) <=> ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(7,plain,
% 0.19/0.41 (![W0: $i] : (aScalar0(W0) => ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00))) <=> ![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[6])).
% 0.19/0.41 tff(8,axiom,(![W0: $i] : (aScalar0(W0) => ((((((((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0)) & (sdtasdt0(W0, sz0z00) = sz0z00)) & (sdtasdt0(sz0z00, W0) = sz0z00)) & (sdtpldt0(W0, smndt0(W0)) = sz0z00)) & (sdtpldt0(smndt0(W0), W0) = sz0z00)) & (smndt0(smndt0(W0)) = W0)) & (smndt0(sz0z00) = sz0z00)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mScZero')).
% 0.19/0.41 tff(9,plain,
% 0.19/0.41 (![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.19/0.41 tff(10,plain,
% 0.19/0.41 (![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.19/0.41 tff(11,plain,(
% 0.19/0.41 ![W0: $i] : ((~aScalar0(W0)) | ((sdtpldt0(W0, sz0z00) = W0) & (sdtpldt0(sz0z00, W0) = W0) & (sdtasdt0(W0, sz0z00) = sz0z00) & (sdtasdt0(sz0z00, W0) = sz0z00) & (sdtpldt0(W0, smndt0(W0)) = sz0z00) & (sdtpldt0(smndt0(W0), W0) = sz0z00) & (smndt0(smndt0(W0)) = W0) & (smndt0(sz0z00) = sz0z00)))),
% 0.19/0.41 inference(skolemize,[status(sab)],[10])).
% 0.19/0.41 tff(12,plain,
% 0.19/0.41 (![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.19/0.41 tff(13,plain,
% 0.19/0.41 (![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[12, 2])).
% 0.19/0.41 tff(14,plain,
% 0.19/0.41 (aScalar0(sz0z00) <=> aScalar0(sz0z00)),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(15,axiom,(aScalar0(sz0z00)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mSZeroSc')).
% 0.19/0.41 tff(16,plain,
% 0.19/0.41 (aScalar0(sz0z00)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.19/0.41 tff(17,plain,
% 0.19/0.41 (((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | ((~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)))))) <=> ((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | (~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)))))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(18,plain,
% 0.19/0.41 (((~aScalar0(sz0z00)) | (~((~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)) | (~(smndt0(sz0z00) = sz0z00))))) <=> ((~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)))))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(19,plain,
% 0.19/0.41 (((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | ((~aScalar0(sz0z00)) | (~((~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)) | (~(smndt0(sz0z00) = sz0z00)))))) <=> ((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | ((~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00))))))),
% 0.19/0.41 inference(monotonicity,[status(thm)],[18])).
% 0.19/0.41 tff(20,plain,
% 0.19/0.41 (((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | ((~aScalar0(sz0z00)) | (~((~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)) | (~(smndt0(sz0z00) = sz0z00)))))) <=> ((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | (~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)))))),
% 0.19/0.41 inference(transitivity,[status(thm)],[19, 17])).
% 0.19/0.41 tff(21,plain,
% 0.19/0.41 ((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | ((~aScalar0(sz0z00)) | (~((~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)) | (~(smndt0(sz0z00) = sz0z00)))))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(22,plain,
% 0.19/0.41 ((~![W0: $i] : ((~aScalar0(W0)) | (~((~(sdtpldt0(W0, sz0z00) = W0)) | (~(sdtpldt0(sz0z00, W0) = W0)) | (~(sdtasdt0(W0, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, W0) = sz0z00)) | (~(sdtpldt0(W0, smndt0(W0)) = sz0z00)) | (~(sdtpldt0(smndt0(W0), W0) = sz0z00)) | (~(smndt0(smndt0(W0)) = W0)) | (~(smndt0(sz0z00) = sz0z00)))))) | (~aScalar0(sz0z00)) | (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00))))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.19/0.41 tff(23,plain,
% 0.19/0.41 (~((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00)))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[22, 16, 13])).
% 0.19/0.41 tff(24,plain,
% 0.19/0.41 (((~(smndt0(sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtasdt0(sz0z00, sz0z00) = sz0z00)) | (~(sdtpldt0(sz0z00, smndt0(sz0z00)) = sz0z00)) | (~(sdtpldt0(smndt0(sz0z00), sz0z00) = sz0z00)) | (~(smndt0(smndt0(sz0z00)) = sz0z00))) | (sdtasdt0(sz0z00, sz0z00) = sz0z00)),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(25,plain,
% 0.19/0.41 (sdtasdt0(sz0z00, sz0z00) = sz0z00),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[24, 23])).
% 0.19/0.41 tff(26,plain,
% 0.19/0.41 ((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) <=> (~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(27,plain,
% 0.19/0.41 ((~(((~(aDimensionOf0(xs) = sz00)) => ?[W0: $i] : ((((aVector0(W0) & (szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(xs))) & ![W1: $i] : (aNaturalNumber0(W1) => (sdtlbdtrb0(W0, W1) = sdtlbdtrb0(xs, W1)))) & (W0 = sziznziztdt0(xs))) & ?[W1: $i] : ((((aVector0(W1) & (szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt))) & ![W2: $i] : (aNaturalNumber0(W2) => (sdtlbdtrb0(W1, W2) = sdtlbdtrb0(xt, W2)))) & (W1 = sziznziztdt0(xt))) & ?[W2: $i] : ((aScalar0(W2) & (W2 = sdtlbdtrb0(xs, aDimensionOf0(xs)))) & ?[W3: $i] : ((aScalar0(W3) & (W3 = sdtlbdtrb0(xt, aDimensionOf0(xt)))) & ?[W4: $i] : ((aScalar0(W4) & (W4 = sdtasasdt0(W0, W0))) & ?[W5: $i] : ((aScalar0(W5) & (W5 = sdtasasdt0(W1, W1))) & ?[W6: $i] : ((aScalar0(W6) & (W6 = sdtasasdt0(W0, W1))) & ?[W7: $i] : ((aScalar0(W7) & (W7 = sdtasdt0(W2, W2))) & ?[W8: $i] : ((aScalar0(W8) & (W8 = sdtasdt0(W3, W3))) & ?[W9: $i] : ((aScalar0(W9) & (W9 = sdtasdt0(W2, W3))) & ?[W10: $i] : ((aScalar0(W10) & (W10 = sdtasdt0(W4, W8))) & ?[W11: $i] : ((aScalar0(W11) & (W11 = sdtasdt0(W6, W9))) & ?[W12: $i] : ((aScalar0(W12) & (W12 = sdtasdt0(W7, W5))) & ?[W13: $i] : (((((aScalar0(W13) & (W13 = sdtasdt0(W10, W12))) & sdtlseqdt0(sdtasdt0(W6, W6), sdtasdt0(W4, W5))) & sdtlseqdt0(sdtpldt0(W11, W11), sdtpldt0(W10, W12))) & sdtlseqdt0(sdtasdt0(sdtpldt0(W6, W9), sdtpldt0(W6, W9)), sdtasdt0(sdtpldt0(W4, W7), sdtpldt0(W5, W8)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))))))))))))))))) => sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))))) <=> (~((~((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(28,axiom,(~(((~(aDimensionOf0(xs) = sz00)) => ?[W0: $i] : ((((aVector0(W0) & (szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(xs))) & ![W1: $i] : (aNaturalNumber0(W1) => (sdtlbdtrb0(W0, W1) = sdtlbdtrb0(xs, W1)))) & (W0 = sziznziztdt0(xs))) & ?[W1: $i] : ((((aVector0(W1) & (szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt))) & ![W2: $i] : (aNaturalNumber0(W2) => (sdtlbdtrb0(W1, W2) = sdtlbdtrb0(xt, W2)))) & (W1 = sziznziztdt0(xt))) & ?[W2: $i] : ((aScalar0(W2) & (W2 = sdtlbdtrb0(xs, aDimensionOf0(xs)))) & ?[W3: $i] : ((aScalar0(W3) & (W3 = sdtlbdtrb0(xt, aDimensionOf0(xt)))) & ?[W4: $i] : ((aScalar0(W4) & (W4 = sdtasasdt0(W0, W0))) & ?[W5: $i] : ((aScalar0(W5) & (W5 = sdtasasdt0(W1, W1))) & ?[W6: $i] : ((aScalar0(W6) & (W6 = sdtasasdt0(W0, W1))) & ?[W7: $i] : ((aScalar0(W7) & (W7 = sdtasdt0(W2, W2))) & ?[W8: $i] : ((aScalar0(W8) & (W8 = sdtasdt0(W3, W3))) & ?[W9: $i] : ((aScalar0(W9) & (W9 = sdtasdt0(W2, W3))) & ?[W10: $i] : ((aScalar0(W10) & (W10 = sdtasdt0(W4, W8))) & ?[W11: $i] : ((aScalar0(W11) & (W11 = sdtasdt0(W6, W9))) & ?[W12: $i] : ((aScalar0(W12) & (W12 = sdtasdt0(W7, W5))) & ?[W13: $i] : (((((aScalar0(W13) & (W13 = sdtasdt0(W10, W12))) & sdtlseqdt0(sdtasdt0(W6, W6), sdtasdt0(W4, W5))) & sdtlseqdt0(sdtpldt0(W11, W11), sdtpldt0(W10, W12))) & sdtlseqdt0(sdtasdt0(sdtpldt0(W6, W9), sdtpldt0(W6, W9)), sdtasdt0(sdtpldt0(W4, W7), sdtpldt0(W5, W8)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))))))))))))))))) => sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__')).
% 0.19/0.42 tff(29,plain,
% 0.19/0.42 (~((~((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.19/0.42 tff(30,plain,
% 0.19/0.42 (~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))),
% 0.19/0.42 inference(or_elim,[status(thm)],[29])).
% 0.19/0.42 tff(31,plain,
% 0.19/0.42 (~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[30, 26])).
% 0.19/0.42 tff(32,plain,
% 0.19/0.42 (((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))))) | sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(33,plain,
% 0.19/0.43 ((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[32, 31])).
% 0.19/0.43 tff(34,plain,
% 0.19/0.43 (((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))))))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(35,plain,
% 0.19/0.43 ((~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) <=> (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))))))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(36,plain,
% 0.19/0.44 (((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))))))),
% 0.19/0.44 inference(monotonicity,[status(thm)],[35])).
% 0.19/0.44 tff(37,plain,
% 0.19/0.44 (((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))))))),
% 0.19/0.45 inference(transitivity,[status(thm)],[36, 34])).
% 0.19/0.45 tff(38,plain,
% 0.19/0.45 (((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(39,plain,
% 0.19/0.45 (((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(40,plain,
% 0.19/0.46 ((aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) <=> (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(41,plain,
% 0.19/0.46 (((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))))),
% 0.19/0.47 inference(monotonicity,[status(thm)],[40])).
% 0.19/0.47 tff(42,plain,
% 0.19/0.47 (((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) <=> ((aDimensionOf0(xs) = sz00) | (~((~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aVector0(sziznziztdt0(xs))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs))) | (~![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1)))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) | (~aVector0(sziznziztdt0(xt))) | (~(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt))) | (~![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2)))) | (~sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt)))) | (~sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)))) | (~aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) | (~sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))) | (~aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)))) | (~aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))))) | (~aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))))),
% 0.19/0.47 inference(transitivity,[status(thm)],[41, 39])).
% 0.19/0.47 tff(43,plain,
% 0.19/0.47 ((aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) <=> (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(44,plain,
% 0.19/0.48 (((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) <=> ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))),
% 0.19/0.48 inference(monotonicity,[status(thm)],[43])).
% 0.19/0.48 tff(45,plain,
% 0.19/0.48 (((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) <=> ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(46,plain,
% 0.19/0.49 ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))),
% 0.19/0.49 inference(or_elim,[status(thm)],[29])).
% 0.19/0.49 tff(47,plain,
% 0.19/0.49 ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[46, 44])).
% 0.19/0.49 tff(48,plain,
% 0.19/0.49 ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[47, 45])).
% 0.19/0.49 tff(49,plain,
% 0.19/0.49 ((aDimensionOf0(xs) = sz00) | (aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aVector0(sziznziztdt0(xs)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)) & ![W1: $i] : ((~aNaturalNumber0(W1)) | (sdtlbdtrb0(sziznziztdt0(xs), W1) = sdtlbdtrb0(xs, W1))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))) & aVector0(sziznziztdt0(xt)) & (szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)) & ![W2: $i] : ((~aNaturalNumber0(W2)) | (sdtlbdtrb0(sziznziztdt0(xt), W2) = sdtlbdtrb0(xt, W2))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtlbdtrb0(xs, aDimensionOf0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtlbdtrb0(xt, aDimensionOf0(xt))) & sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtpldt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs))) & aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))) & aScalar0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt))) & sdtlseqdt0(sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xt, aDimensionOf0(xt))))), sdtasdt0(sdtpldt0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xs)), sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))), sdtpldt0(sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)), sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))) & aScalar0(sdtasasdt0(sziznziztdt0(xs), sziznziztdt0(xt))) & aScalar0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs))), sdtasasdt0(sziznziztdt0(xt), sziznziztdt0(xt)))) & aScalar0(sdtasdt0(sdtlbdtrb0(xs, aDimensionOf0(xs)), sdtlbdtrb0(xs, aDimensionOf0(xs)))) & sdtlseqdt0(sdtasdt0(sdtasasdt0(xs, xt), sdtasasdt0(xs, xt)), sdtasdt0(sdtasasdt0(xs, xs), sdtasasdt0(xt, xt))) & aScalar0(sdtasdt0(sdtlbdtrb0(xt, aDimensionOf0(xt)), sdtlbdtrb0(xt, aDimensionOf0(xt)))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[48, 44])).
% 0.19/0.49 Proof display could not be completed: monotonicity rule is not handled
% 0.19/0.50 % E exiting
%------------------------------------------------------------------------------