Theorem pw2cut2

Description: Cut expression for powers of two. Theorem 12 of Conway p. 12-13. (Contributed by Scott Fenton, 18-Jan-2026)

	Ref	Expression
Assertion	pw2cut2	Could not format assertion : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	Could not format ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) with typecode |-
2		2no	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
3		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
4	2 3	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
5	1 4	eqtrdi	Could not format ( m = 0s -> ( 2s ^su m ) = 1s ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = 1s ) with typecode |-
6	5	oveq2d	Could not format ( m = 0s -> ( A /su ( 2s ^su m ) ) = ( A /su 1s ) ) : No typesetting found for |- ( m = 0s -> ( A /su ( 2s ^su m ) ) = ( A /su 1s ) ) with typecode |-
7	5	oveq2d	Could not format ( m = 0s -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su 1s ) ) : No typesetting found for |- ( m = 0s -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su 1s ) ) with typecode |-
8	7	sneqd	Could not format ( m = 0s -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su 1s ) } ) : No typesetting found for |- ( m = 0s -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su 1s ) } ) with typecode |-
9	5	oveq2d	Could not format ( m = 0s -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su 1s ) ) : No typesetting found for |- ( m = 0s -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su 1s ) ) with typecode |-
10	9	sneqd	Could not format ( m = 0s -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su 1s ) } ) : No typesetting found for |- ( m = 0s -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su 1s ) } ) with typecode |-
11	8 10	oveq12d	Could not format ( m = 0s -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) : No typesetting found for |- ( m = 0s -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) with typecode |-
12	6 11	eqeq12d	Could not format ( m = 0s -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) ) : No typesetting found for |- ( m = 0s -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) ) with typecode |-
13	12	imbi2d	Could not format ( m = 0s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) ) ) : No typesetting found for |- ( m = 0s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su 1s ) = ( { ( ( A -s 1s ) /su 1s ) } |s { ( ( A +s 1s ) /su 1s ) } ) ) ) ) with typecode |-
14		oveq2	Could not format ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) : No typesetting found for |- ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) with typecode |-
15	14	oveq2d	Could not format ( m = n -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( m = n -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
16	14	oveq2d	Could not format ( m = n -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) ) : No typesetting found for |- ( m = n -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) ) with typecode |-
17	16	sneqd	Could not format ( m = n -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } ) : No typesetting found for |- ( m = n -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } ) with typecode |-
18	14	oveq2d	Could not format ( m = n -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) ) : No typesetting found for |- ( m = n -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) ) with typecode |-
19	18	sneqd	Could not format ( m = n -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) : No typesetting found for |- ( m = n -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) with typecode |-
20	17 19	oveq12d	Could not format ( m = n -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( m = n -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
21	15 20	eqeq12d	Could not format ( m = n -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( m = n -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
22	21	imbi2d	Could not format ( m = n -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) : No typesetting found for |- ( m = n -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) with typecode |-
23		oveq2	Could not format ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) with typecode |-
24	23	oveq2d	Could not format ( m = ( n +s 1s ) -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
25	23	oveq2d	Could not format ( m = ( n +s 1s ) -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
26	25	sneqd	Could not format ( m = ( n +s 1s ) -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) : No typesetting found for |- ( m = ( n +s 1s ) -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) with typecode |-
27	23	oveq2d	Could not format ( m = ( n +s 1s ) -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
28	27	sneqd	Could not format ( m = ( n +s 1s ) -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) : No typesetting found for |- ( m = ( n +s 1s ) -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) with typecode |-
29	26 28	oveq12d	Could not format ( m = ( n +s 1s ) -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
30	24 29	eqeq12d	Could not format ( m = ( n +s 1s ) -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
31	30	imbi2d	Could not format ( m = ( n +s 1s ) -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
32		oveq2	Could not format ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) : No typesetting found for |- ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) with typecode |-
33	32	oveq2d	Could not format ( m = N -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su N ) ) ) : No typesetting found for |- ( m = N -> ( A /su ( 2s ^su m ) ) = ( A /su ( 2s ^su N ) ) ) with typecode |-
34	32	oveq2d	Could not format ( m = N -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su N ) ) ) : No typesetting found for |- ( m = N -> ( ( A -s 1s ) /su ( 2s ^su m ) ) = ( ( A -s 1s ) /su ( 2s ^su N ) ) ) with typecode |-
35	34	sneqd	Could not format ( m = N -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su N ) ) } ) : No typesetting found for |- ( m = N -> { ( ( A -s 1s ) /su ( 2s ^su m ) ) } = { ( ( A -s 1s ) /su ( 2s ^su N ) ) } ) with typecode |-
36	32	oveq2d	Could not format ( m = N -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su N ) ) ) : No typesetting found for |- ( m = N -> ( ( A +s 1s ) /su ( 2s ^su m ) ) = ( ( A +s 1s ) /su ( 2s ^su N ) ) ) with typecode |-
37	36	sneqd	Could not format ( m = N -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) : No typesetting found for |- ( m = N -> { ( ( A +s 1s ) /su ( 2s ^su m ) ) } = { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) with typecode |-
38	35 37	oveq12d	Could not format ( m = N -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) : No typesetting found for |- ( m = N -> ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) with typecode |-
39	33 38	eqeq12d	Could not format ( m = N -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) : No typesetting found for |- ( m = N -> ( ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) <-> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) with typecode |-
40	39	imbi2d	Could not format ( m = N -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) ) : No typesetting found for |- ( m = N -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su m ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su m ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su m ) ) } ) ) <-> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) ) with typecode |-
41		zcuts	$$⊢A\in {\mathbb{Z}}_s\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
42		zno	$$⊢A\in {\mathbb{Z}}_s\to A\in \mathrm{No}$$
43	42	divs1d	$$⊢A\in {\mathbb{Z}}_s\to A{/}_{\mathrm{su}}{1}_s=A$$
44		1no	$$⊢1_s\in \mathrm{No}$$
45	44	a1i	$$⊢A\in {\mathbb{Z}}_s\to 1_s\in \mathrm{No}$$
46	42 45	subscld	$$⊢A\in {\mathbb{Z}}_s\to A{-}_s{1}_s\in \mathrm{No}$$
47	46	divs1d	$$⊢A\in {\mathbb{Z}}_s\to \left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{-}_s{1}_s$$
48	47	sneqd	$$⊢A\in {\mathbb{Z}}_s\to \left\{\left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}=\left\{A{-}_s{1}_s\right\}$$
49	42 45	addscld	$$⊢A\in {\mathbb{Z}}_s\to A{+}_s{1}_s\in \mathrm{No}$$
50	49	divs1d	$$⊢A\in {\mathbb{Z}}_s\to \left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{+}_s{1}_s$$
51	50	sneqd	$$⊢A\in {\mathbb{Z}}_s\to \left\{\left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}=\left\{A{+}_s{1}_s\right\}$$
52	48 51	oveq12d	$$⊢A\in {\mathbb{Z}}_s\to \left\{\left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}{|}_s\left\{\left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
53	41 43 52	3eqtr4d	$$⊢A\in {\mathbb{Z}}_s\to A{/}_{\mathrm{su}}{1}_s=\left\{\left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}{|}_s\left\{\left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s\right\}$$
54		simp2	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. ZZ_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. ZZ_s ) with typecode |-
55	54	znod	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A e. No ) with typecode |-
56	44	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. No ) with typecode |-
57	55 56	subscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s ) e. No ) with typecode |-
58		simp1	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> n e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> n e. NN0_s ) with typecode |-
59		peano2n0s	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
60	58 59	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( n +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( n +s 1s ) e. NN0_s ) with typecode |-
61	57 60	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
62	55 56	addscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s 1s ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s 1s ) e. No ) with typecode |-
63	62 60	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
64	55	ltsm1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s ) ( A -s 1s )
65	55	ltsp1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A A
66	57 55 62 64 65	ltstrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A -s 1s ) ( A -s 1s )
67	57 62 60	pw2ltsdiv1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( A -s 1s ) ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
68	66 67	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
69	61 63 68	sltssn	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
70	69	cutscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No ) with typecode |-
71	61 70	addscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) with typecode |-
72	63 70	addscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) with typecode |-
73	61 63 70	ltadds1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
74	68 73	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
75	71 72 74	sltssn	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
76	57 58	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) e. No ) with typecode |-
77	62 58	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) e. No ) with typecode |-
78	57 62 58	pw2ltsdiv1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) ( ( A -s 1s ) /su ( 2s ^su n ) ) ( ( A -s 1s ) ( ( A -s 1s ) /su ( 2s ^su n ) )
79	66 78	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) ( ( A -s 1s ) /su ( 2s ^su n ) )
80	76 77 79	sltssn	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su n ) ) } < { ( ( A -s 1s ) /su ( 2s ^su n ) ) } <
81		eqidd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) with typecode |-
82		simp3	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
83	55 58	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) e. No ) with typecode |-
84		cutcuts	Could not format ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
85	69 84	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No /\ { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
86	85	simp3d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } < { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } <
87		ovex	Could not format ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. _V : No typesetting found for |- ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. _V with typecode |-
88	87	snid	Could not format ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } : No typesetting found for |- ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } with typecode |-
89	88	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. { ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) } ) with typecode |-
90		ovex	Could not format ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V : No typesetting found for |- ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V with typecode |-
91	90	snid	Could not format ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } : No typesetting found for |- ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } with typecode |-
92	91	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) with typecode |-
93	86 89 92	sltssepcd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } )
94	70 63 61	ltadds2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
95	93 94	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
96	55 55 56	addsassd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s A ) +s 1s ) = ( A +s ( A +s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s A ) +s 1s ) = ( A +s ( A +s 1s ) ) ) with typecode |-
97	96	oveq1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( ( A +s ( A +s 1s ) ) -s 1s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( ( A +s ( A +s 1s ) ) -s 1s ) ) with typecode |-
98	55 55	addscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s A ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A +s A ) e. No ) with typecode |-
99		pncans	$$⊢\left(A{+}_{s}A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(\left(A{+}_{s}A\right){+}_s{1}_s\right){-}_s{1}_s=A{+}_{s}A$$
100	98 44 99	sylancl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( A +s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( A +s A ) ) with typecode |-
101		no2times	Could not format ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
102	55 101	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
103	100 102	eqtr4d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) with typecode |-
104	55 62 56	addsubsd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s ( A +s 1s ) ) -s 1s ) = ( ( A -s 1s ) +s ( A +s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s ( A +s 1s ) ) -s 1s ) = ( ( A -s 1s ) +s ( A +s 1s ) ) ) with typecode |-
105	97 103 104	3eqtr3rd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) +s ( A +s 1s ) ) = ( 2s x.s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) +s ( A +s 1s ) ) = ( 2s x.s A ) ) with typecode |-
106	105	oveq1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
107	57 62 60	pw2divsdird	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
108		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
109	108	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 1s e. NN0_s ) with typecode |-
110	55 58 109	pw2divscan4d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
111		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
112	2 111	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
113	112	oveq1i	Could not format ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A ) with typecode |-
114	113	oveq1i	Could not format ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) with typecode |-
115	110 114	eqtr2di	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
116	106 107 115	3eqtr3d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
117	95 116	breqtrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
118	71 83 117	sltssn	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
119	63 61	addscomd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
120	119 116	eqtrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
121	85	simp2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } < { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } <
122		ovex	Could not format ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V : No typesetting found for |- ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. _V with typecode |-
123	122	snid	Could not format ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } : No typesetting found for |- ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } with typecode |-
124	123	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) with typecode |-
125	121 124 89	sltssepcd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) )
126	61 70 63	ltadds2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
127	125 126	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
128	120 127	eqbrtrrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su n ) ) ( A /su ( 2s ^su n ) )
129	83 72 128	sltssn	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { ( A /su ( 2s ^su n ) ) } < { ( A /su ( 2s ^su n ) ) } <
130	57 58 109	pw2divscan4d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
131	112	oveq1i	Could not format ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( 2s x.s ( A -s 1s ) ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( 2s x.s ( A -s 1s ) ) with typecode |-
132		no2times	Could not format ( ( A -s 1s ) e. No -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) : No typesetting found for |- ( ( A -s 1s ) e. No -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) with typecode |-
133	57 132	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) with typecode |-
134	131 133	eqtrid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) = ( ( A -s 1s ) +s ( A -s 1s ) ) ) with typecode |-
135	134	oveq1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
136	57 57 60	pw2divsdird	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) +s ( A -s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
137	130 135 136	3eqtrrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A -s 1s ) /su ( 2s ^su n ) ) ) with typecode |-
138	61 70 61	ltadds2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
139	125 138	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) )
140	137 139	eqbrtrrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A -s 1s ) /su ( 2s ^su n ) ) ( ( A -s 1s ) /su ( 2s ^su n ) )
141		ltsasym	Could not format ( ( ( ( A -s 1s ) /su ( 2s ^su n ) ) e. No /\ ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No ) -> ( ( ( A -s 1s ) /su ( 2s ^su n ) ) -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su n ) ) -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
142	76 71 141	syl2anc	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A -s 1s ) /su ( 2s ^su n ) ) -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A -s 1s ) /su ( 2s ^su n ) ) -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
143	140 142	mpd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) -. ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
144	71 76	sltssnb	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
145	143 144	mtbird	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
146	145	intnanrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
147		ovex	Could not format ( ( A -s 1s ) /su ( 2s ^su n ) ) e. _V : No typesetting found for |- ( ( A -s 1s ) /su ( 2s ^su n ) ) e. _V with typecode |-
148		sneq	Could not format ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } ) : No typesetting found for |- ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A -s 1s ) /su ( 2s ^su n ) ) } ) with typecode |-
149	148	breq2d	Could not format ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
150	148	breq1d	Could not format ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A -s 1s ) /su ( 2s ^su n ) ) } < ( { xO } < { ( ( A -s 1s ) /su ( 2s ^su n ) ) } <
151	149 150	anbi12d	Could not format ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
152	151	notbid	Could not format ( xO = ( ( A -s 1s ) /su ( 2s ^su n ) ) -> ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
153	147 152	ralsn	Could not format ( A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
154	146 153	sylibr	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
155	70 63 63	ltadds2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
156	93 155	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
157	62 58 109	pw2divscan4d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( A +s 1s ) /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
158	112	oveq1i	Could not format ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( 2s x.s ( A +s 1s ) ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( 2s x.s ( A +s 1s ) ) with typecode |-
159		no2times	Could not format ( ( A +s 1s ) e. No -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) : No typesetting found for |- ( ( A +s 1s ) e. No -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) with typecode |-
160	62 159	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) with typecode |-
161	158 160	eqtrid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) = ( ( A +s 1s ) +s ( A +s 1s ) ) ) with typecode |-
162	161	oveq1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( 2s ^su 1s ) x.s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
163	62 62 60	pw2divsdird	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) +s ( A +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
164	157 162 163	3eqtrrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( A +s 1s ) /su ( 2s ^su n ) ) ) with typecode |-
165	156 164	breqtrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) )
166		ltsasym	Could not format ( ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) e. No /\ ( ( A +s 1s ) /su ( 2s ^su n ) ) e. No ) -> ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) -. ( ( A +s 1s ) /su ( 2s ^su n ) ) ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) -. ( ( A +s 1s ) /su ( 2s ^su n ) )
167	72 77 166	syl2anc	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) -. ( ( A +s 1s ) /su ( 2s ^su n ) ) ( ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) -. ( ( A +s 1s ) /su ( 2s ^su n ) )
168	165 167	mpd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( ( A +s 1s ) /su ( 2s ^su n ) ) -. ( ( A +s 1s ) /su ( 2s ^su n ) )
169	77 72	sltssnb	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A +s 1s ) /su ( 2s ^su n ) ) } < ( ( A +s 1s ) /su ( 2s ^su n ) ) ( { ( ( A +s 1s ) /su ( 2s ^su n ) ) } < ( ( A +s 1s ) /su ( 2s ^su n ) )
170	168 169	mtbird	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } < -. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } <
171	170	intnand	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
172		ovex	Could not format ( ( A +s 1s ) /su ( 2s ^su n ) ) e. _V : No typesetting found for |- ( ( A +s 1s ) /su ( 2s ^su n ) ) e. _V with typecode |-
173		sneq	Could not format ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) : No typesetting found for |- ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> { xO } = { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) with typecode |-
174	173	breq2d	Could not format ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
175	173	breq1d	Could not format ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( { xO } < { ( ( A +s 1s ) /su ( 2s ^su n ) ) } < ( { xO } < { ( ( A +s 1s ) /su ( 2s ^su n ) ) } <
176	174 175	anbi12d	Could not format ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
177	176	notbid	Could not format ( xO = ( ( A +s 1s ) /su ( 2s ^su n ) ) -> ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
178	172 177	ralsn	Could not format ( A. xO e. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
179	171 178	sylibr	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < A. xO e. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
180		ralunb	Could not format ( A. xO e. ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } u. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < ( A. xO e. { ( ( A -s 1s ) /su ( 2s ^su n ) ) } -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
181	154 179 180	sylanbrc	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> A. xO e. ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } u. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } < A. xO e. ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } u. { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -. ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } <
182	75 80 81 82 118 129 181	eqcuts3	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
183		no2times	Could not format ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) e. No -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
184	70 183	syl	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
185		eqidd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
186	69 69 185 185	addsunif	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) ) with typecode |-
187		oveq1	Could not format ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
188	187	eqeq2d	Could not format ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
189	122 188	rexsn	Could not format ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
190	189	abbii	Could not format { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
191	190	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
192		oveq2	Could not format ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
193	192	eqeq2d	Could not format ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) ) : No typesetting found for |- ( b = ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) ) with typecode |-
194	122 193	rexsn	Could not format ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
195	70 61	addscomd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
196	195	eqeq2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
197	194 196	bitrid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
198	197	abbidv	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
199	191 198	uneq12d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) with typecode |-
200		unidm	Could not format ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
201		df-sn	Could not format { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
202	200 201	eqtr4i	Could not format ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- ( { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
203	199 202	eqtrdi	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
204		oveq1	Could not format ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
205	204	eqeq2d	Could not format ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
206	90 205	rexsn	Could not format ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
207	206	abbii	Could not format { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
208	207	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
209		oveq2	Could not format ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
210	209	eqeq2d	Could not format ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) ) : No typesetting found for |- ( b = ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) ) with typecode |-
211	90 210	rexsn	Could not format ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
212	70 63	addscomd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
213	212	eqeq2d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
214	211 213	bitrid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) <-> a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
215	214	abbidv	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
216	208 215	uneq12d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) with typecode |-
217		unidm	Could not format ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
218		df-sn	Could not format { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } = { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
219	217 218	eqtr4i	Could not format ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } : No typesetting found for |- ( { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | a = ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } with typecode |-
220	216 219	eqtrdi	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) = { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) with typecode |-
221	203 220	oveq12d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) |s ( { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( b +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } u. { a | E. b e. { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } a = ( ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) +s b ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) with typecode |-
222	184 186 221	3eqtrd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( { ( ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } |s { ( ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) +s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) } ) ) with typecode |-
223	2	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s e. No ) with typecode |-
224	223 55 60	pw2divsassd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) = ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
225	114 224	eqtr2id	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( ( ( 2s ^su 1s ) x.s A ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
226	225 110	eqtr4d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( A /su ( 2s ^su n ) ) ) with typecode |-
227	182 222 226	3eqtr4rd	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
228	55 60	pw2divscld	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
229		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
230	229	a1i	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s =/= 0s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> 2s =/= 0s ) with typecode |-
231	228 70 223 230	mulscan1d	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( ( 2s x.s ( A /su ( 2s ^su ( n +s 1s ) ) ) ) = ( 2s x.s ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) <-> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) with typecode |-
232	227 231	mpbid	Could not format ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. ZZ_s /\ ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
233	232	3exp	Could not format ( n e. NN0_s -> ( A e. ZZ_s -> ( ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( A e. ZZ_s -> ( ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
234	233	a2d	Could not format ( n e. NN0_s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( ( A e. ZZ_s -> ( A /su ( 2s ^su n ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su n ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su n ) ) } ) ) -> ( A e. ZZ_s -> ( A /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) ) ) with typecode |-
235	13 22 31 40 53 234	n0sind	Could not format ( N e. NN0_s -> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. ZZ_s -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) ) with typecode |-
236	235	impcom	Could not format ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A /su ( 2s ^su N ) ) = ( { ( ( A -s 1s ) /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) ) with typecode |-