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		2sno	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		zscut	$$⊢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		divs1	$$⊢A\in \mathrm{No}\to A{/}_{\mathrm{su}}{1}_s=A$$
44	42 43	syl	$$⊢A\in {\mathbb{Z}}_s\to A{/}_{\mathrm{su}}{1}_s=A$$
45		1sno	$$⊢1_s\in \mathrm{No}$$
46	45	a1i	$$⊢A\in {\mathbb{Z}}_s\to 1_s\in \mathrm{No}$$
47	42 46	subscld	$$⊢A\in {\mathbb{Z}}_s\to A{-}_s{1}_s\in \mathrm{No}$$
48		divs1	$$⊢A{-}_s{1}_s\in \mathrm{No}\to \left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{-}_s{1}_s$$
49	47 48	syl	$$⊢A\in {\mathbb{Z}}_s\to \left(A{-}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{-}_s{1}_s$$
50	49	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\}$$
51	42 46	addscld	$$⊢A\in {\mathbb{Z}}_s\to A{+}_s{1}_s\in \mathrm{No}$$
52		divs1	$$⊢A{+}_s{1}_s\in \mathrm{No}\to \left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{+}_s{1}_s$$
53	51 52	syl	$$⊢A\in {\mathbb{Z}}_s\to \left(A{+}_s{1}_s\right){/}_{\mathrm{su}}{1}_s=A{+}_s{1}_s$$
54	53	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\}$$
55	50 54	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\}$$
56	41 44 55	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\}$$
57		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 |-
58	57	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 |-
59	45	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 |-
60	58 59	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 |-
61		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 |-
62		peano2n0s	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
63	61 62	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 |-
64	60 63	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 |-
65	58 59	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 |-
66	65 63	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 |-
67	58	sltm1d	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 )
68	58	sltp1d	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
69	60 58 65 67 68	slttrd	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 )
70	60 65 63	pw2sltdiv1d	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 ) ) )
71	69 70	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 ) ) )
72	64 66 71	ssltsn	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 ) ) ) } <
73	72	scutcld	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 |-
74	64 73	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 |-
75	66 73	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 |-
76	64 66 73	sltadd1d	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 ) ) ) } ) )
77	71 76	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 ) ) ) } ) )
78	74 75 77	ssltsn	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 ) ) ) } ) ) } <
79	60 61	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 |-
80	65 61	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 |-
81	60 65 61	pw2sltdiv1d	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 ) )
82	69 81	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 ) )
83	79 80 82	ssltsn	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 ) ) } <
84		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 |-
85		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 |-
86	58 61	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 |-
87		scutcut	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 ) ) ) } <
88	72 87	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 ) ) ) } <
89	88	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 ) ) ) } ) } <
90		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 |-
91	90	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 |-
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 ) ) ) } |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 |-
93		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 |-
94	93	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 |-
95	94	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 |-
96	89 92 95	ssltsepcd	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 ) ) ) } )
97	73 66 64	sltadd2d	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 ) ) ) } ) )
98	96 97	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 ) ) ) } ) )
99	58 58 59	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 |-
100	99	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 |-
101	58 58	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 |-
102		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$$
103	101 45 102	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 |-
104		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 |-
105	58 104	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 |-
106	103 105	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 |-
107	58 65 59	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 |-
108	100 106 107	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 |-
109	108	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 |-
110	60 65 63	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 |-
111		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
112	111	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 |-
113	58 61 112	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 |-
114		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
115	2 114	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
116	115	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 |-
117	116	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 |-
118	113 117	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 |-
119	109 110 118	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 |-
120	98 119	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 ) ) ) } ) )
121	74 86 120	ssltsn	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 ) ) ) } ) ) } <
122	66 64	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 |-
123	122 119	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 |-
124	88	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 ) ) ) } <
125		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 |-
126	125	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 |-
127	126	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 |-
128	124 127 92	ssltsepcd	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 ) ) )
129	64 73 66	sltadd2d	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 ) ) ) )
130	128 129	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 ) ) ) )
131	123 130	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 ) )
132	86 75 131	ssltsn	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 ) ) } <
133	60 61 112	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 |-
134	115	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 |-
135		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 |-
136	60 135	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 |-
137	134 136	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 |-
138	137	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 |-
139	60 60 63	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 |-
140	133 138 139	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 |-
141	64 73 64	sltadd2d	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 ) ) ) )
142	128 141	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 ) ) ) )
143	140 142	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 ) )
144		sltasym	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 ) ) ) } ) )
145	79 74 144	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 ) ) ) } ) )
146	143 145	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 ) ) ) } ) )
147	74 79	ssltsnb	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 ) ) ) } ) )
148	146 147	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 ) ) ) } ) ) } <
149	148	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 ) ) ) } ) ) } <
150		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 |-
151		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 |-
152	151	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 ) ) ) } ) ) } <
153	151	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 ) ) } <
154	152 153	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 ) ) ) } ) ) } <
155	154	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 ) ) ) } ) ) } <
156	150 155	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 ) ) ) } ) ) } <
157	149 156	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 ) ) ) } ) ) } <
158	73 66 66	sltadd2d	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 ) ) ) } ) )
159	96 158	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 ) ) ) } ) )
160	65 61 112	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 |-
161	115	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 |-
162		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 |-
163	65 162	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 |-
164	161 163	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 |-
165	164	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 |-
166	65 65 63	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 |-
167	160 165 166	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 |-
168	159 167	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 ) ) ) } ) )
169		sltasym	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 ) )
170	75 80 169	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 ) )
171	168 170	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 ) )
172	80 75	ssltsnb	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 ) )
173	171 172	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 ) ) } <
174	173	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 ) ) ) } ) ) } <
175		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 |-
176		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 |-
177	176	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 ) ) ) } ) ) } <
178	176	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 ) ) } <
179	177 178	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 ) ) ) } ) ) } <
180	179	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 ) ) ) } ) ) } <
181	175 180	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 ) ) ) } ) ) } <
182	174 181	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 ) ) ) } ) ) } <
183		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 ) ) ) } ) ) } <
184	157 182 183	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 ) ) ) } ) ) } <
185	78 83 84 85 121 132 184	eqscut3	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 |-
186		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 |-
187	73 186	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 |-
188		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 |-
189	72 72 188 188	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 |-
190		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 |-
191	190	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 |-
192	125 191	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 |-
193	192	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 |-
194	193	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 |-
195		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 |-
196	195	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 |-
197	125 196	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 |-
198	73 64	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 |-
199	198	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 |-
200	197 199	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 |-
201	200	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 |-
202	194 201	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 |-
203		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 |-
204		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 |-
205	203 204	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 |-
206	202 205	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 |-
207		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 |-
208	207	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 |-
209	93 208	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 |-
210	209	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 |-
211	210	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 |-
212		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 |-
213	212	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 |-
214	93 213	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 |-
215	73 66	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 |-
216	215	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 |-
217	214 216	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 |-
218	217	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 |-
219	211 218	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 |-
220		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 |-
221		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 |-
222	220 221	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 |-
223	219 222	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 |-
224	206 223	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 |-
225	187 189 224	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 |-
226	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 |-
227	226 58 63	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 |-
228	117 227	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 |-
229	228 113	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 |-
230	185 225 229	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 |-
231	58 63	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 |-
232		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
233	232	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 |-
234	231 73 226 233	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 |-
235	230 234	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 |-
236	235	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 |-
237	236	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 |-
238	13 22 31 40 56 237	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 |-
239	238	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 |-