-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcla_adder.tex
317 lines (261 loc) · 17.3 KB
/
cla_adder.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
\documentclass{article}
\usepackage{lipsum,amsmath, amssymb, amsthm, tikz}
\title{Specifying and Verifying a Carry-Look-Ahead Adder for the Lambda32 Processor}
\author{Amjad Ali}
\newtheorem{lemma}{Lemma}
\begin{document}
\maketitle
\begin{abstract}
\lipsum[1]
\end{abstract}
\section{Introduction}
\lipsum[1-2]
\section{Preliminaries}
In this section, we introduce the fundamental building blocks that are essential throughout our proof. Let us begin by defining a carry-out and sum output of a typical 1-bit full-adder. In a standard 1-bit full-adder architecture, there are three inputs: a and b represent the primary operands, and c serves as the carry-in.
\noindent \textbf{Definition 2.1} Suppose $a$, $b$, and $c$ are propositions. Then, carry-out and sum are denoted by the following predicates:
\begin{enumerate}
\item $CO(a, b, c) :\equiv (a \land b) \lor (a \land c) \lor (b \land c)$
\item $S(a, b, c) :\equiv
(a \land b \land c) \lor
(a \land \lnot b \land \lnot c) \lor
(\lnot a \land b \land \lnot c) \lor
(\lnot a \land \lnot b \land c) $
\end{enumerate}
In a standard 1-bit full-adder, the carry-out is $True$ when two, or all, of its operands are $True$. Further scrutiny of our minimal definition of $CO$ shows it conforms with this behavior:
\noindent \textbf{Lemma 2.1} $ (\forall a, b, c \in \{T, F\}) \: CO(a, b, c) \iff (\lnot a \land b \land c) \lor (a \land \lnot b \land c) \lor \\ (a \land b \land \lnot c) \lor (a \land b \land c)$
\begin{proof}
\begin{align*}
(1) & \quad (\lnot a \land b \land c) \lor (a \land \lnot b \land c) \lor (a \land b \land \lnot c) \lor (a \land b \land c) & \text{Assump} \\
(2) & \quad (b \land c) \land (\lnot a \lor a) \lor (a \land \lnot b \land c) \lor (a \land b \land \lnot c) & \text{Distrib} \\
(3) & \quad (b \land c) \lor (a \land \lnot b \land c) \lor (a \land b \land \lnot c) & \text{Compl} \\
(4) & \quad (c \land (b \lor (a \land \lnot b))) \lor (a \land b \land \lnot c) & \text{Distrib} \\
(5) & \quad (c \land (b \lor a \land b \lor \lnot b)) \lor (a \land b \land \lnot c) & \text{Distrib} \\
(6) & \quad (c \land (b \lor a)) \lor (a \land b \land \lnot c) & \text{Compl} \\
(7) & \quad (c \land b) \lor (c \land a) \lor (a \land b \land \lnot c) & \text{Distrib} \\
(8) & \quad (b \land (c \lor (a \land \lnot c)) \lor (c \land a) & \text{Distrib} \\
(9) & \quad (b \land (c \lor a)) \lor (c \land a) & \text{Distrib, Compl} \\
(10) & \quad (a \land b) \lor (a \land c) \lor (b \land c) & \text{Distrib, Commut} \\
(11) & \quad CO(a, b, c) \iff CO(a, b, c) & \text{Tauto} \\
\end{align*}
\end{proof}
The $S$ output in a conventional full-adder should result to $True$ when exactly one, or all, of its inputs are $True$. Since our proposed definition of $S$ was not simplified, no further justification is necessary. We will now build upon our previous definitions to specify a standard $N$-bit carry-ripple adder.
\newpage
\noindent \textbf{Definition 2.2} Suppose $a_n$, $a_{n-1}$, $\ldots$, $a_0$, $b_n$, $b_{n-1}$, $\ldots$, $b_0$, and $c$ are propositions for any integer $ n \geq 0$. Then, carry-out and sum outputs of an $N$-bit carry-ripple adder are defined as follows:
\begin{enumerate}
\item $ CRACO(a_n, \ldots, a_0, b_n, \ldots, b_0, c) :\equiv CO(a_n, b_n, CO(\ldots, CO(a_0, b_0, c))\ldots)$
\item $ CRAS(a_n, \ldots, a_0, b_n, \ldots, b_0, c) :\equiv S(a_n, b_n, CRACO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) $
\end{enumerate}
This definition highlights the recursive nature of \( CRACO \) and, by extension, \( CRAS \). This recursive structure arises because the output of each full-adder in a carry-ripple configuration depends on the carry-out of its preceding full-adders. With the essential building blocks defined, we can now delve into the details of our carry-look-ahead adder.
\section{Carry-Look-Ahead Adder}
Carry-look-ahead adders reduce the delays inherent in traditional carry-ripple configurations. They accomplish this by pre-calculating the carry-out dependencies. However, due to their complexity and size, we will focus only on a 2-bit design, effectively halving our adder's state count.
\noindent \textbf{Definition 3.1} Suppose $a_1$, $a_0$, $b_1$, $b_0$, and $c$ are propositions. Then, the first sum, second sum, and carry-out outputs for our 2-bit carry-look-ahead adder are defined as follows:
\begin{enumerate}
\item
$ CLAS_0(a_0, b_0, c) :\equiv $
\begin{align*}
&(a_0 \land b_0 \land c) \lor
(a_0 \land \lnot b_0 \land \lnot c) \lor
(\lnot a_0 \land b_0 \land \lnot c) \lor
(\lnot a_0 \land \lnot b_0 \land c)
\end{align*}
\item
$ CLAS_1(a_1, a_0, b_1, b_0, c) :\equiv $
\begin{align*}
& (a_1 \land a_0 \land b_1 \land b_0) \lor && \text{ \tiny (1)} \\
& (a_1 \land a_0 \land b_1 \land c) \lor && \text{ \tiny (2)} \\
& (a_1 \land b_1 \land b_0 \land c) \lor && \text{ \tiny (3)} \\
& (a_1 \land \lnot a_0 \land \lnot b_1 \land \lnot b_0) \lor && \text{ \tiny (4)} \\
& (a_1 \land \lnot a_0 \land \lnot b_1 \land \lnot c) \lor && \text{ \tiny (5)} \\
& (a_1 \land \lnot b_1 \land \lnot b_0 \land \lnot c) \lor && \text{ \tiny (6)} \\
& (\lnot a_1 \land a_0 \land \lnot b_1 \land b_0) \lor && \text{ \tiny (7)} \\
& (\lnot a_1 \land a_0 \land \lnot b_1 \land c) \lor && \text{ \tiny (8)} \\
& (\lnot a_1 \land b_1 \land \lnot b_0 \land \lnot c) \lor && \text{ \tiny (9)} \\
& (\lnot a_1 \land \lnot a_0 \land b_1 \land \lnot b_0) \lor && \text{ \tiny (10)} \\
& (\lnot a_1 \land \lnot a_0 \land b_1 \land \lnot c) \lor && \text{ \tiny (11)} \\
& (\lnot a_1 \land \lnot b_1 \land b_0 \land c) && \text{ \tiny (12)}
\end{align*}
\newpage
\item
$ CLACO(a_1, a_0, b_1, b_0, c) :\equiv $
\begin{align*}
& (a_1 \land a_0 \land b_0) \lor
(a_1 \land a_0 \land c) \lor \\
& (a_1 \land b_0 \land c) \lor
(a_1 \land b_1) \lor \\
& (a_0 \land b_1 \land c) \lor
(a_0 \land b_1 \land b_0) \lor \\
& (b_1 \land b_0 \land c)
\end{align*}
\end{enumerate}
\noindent \textbf{Lemma 3.1} $ (\forall a, b, c \in \{T, F\}) \: CLAS_0(a, b, c) \iff S(a, b, c) $
\begin{proof}
\begin{align*}
(\lnot a \land \lnot b \land c) \lor (\lnot a \land b \land \lnot c) \lor
(a \land \lnot b \land \lnot c) \lor (a \land b \land c)
\\ \iff (\lnot a \land \lnot b \land c) \lor
(\lnot a \land b \land \lnot c) \lor
(a \land \lnot b \land \lnot c) \lor (a \land b \land c) \\
& \text{Tauto}
\end{align*}
\end{proof}
\noindent \textbf{Lemma 3.2} $ (\forall a_1, a_0, b_1, b_0, c \in \{T, F\}) \; CLAS_1(a_1, a_0, b_1, b_0, c) \iff S(a_1, b_1, CO(a_0, b_0, c)) $
\begin{proof}
Given the complex structure of $CLAS_1$, we will approach the proof in more manageable steps. By expanding the formula $ S(a_1, b_1, CO(a_0, b_0, c)) $, we aim to demonstrate a bijective relationship: each individual disjunction in $ S(a_1, b_1, CO(a_0, b_0, c)) $ corresponds precisely to a unique disjunction in $ CLAS_1(a_1, a_0, b_1, b_0, c) $, and vice versa. The labels in the $ CLAS_1 $ definition will provide a clear reference for this correspondence.
\begin{align*}
S(a_1, b_1, CO(a_0, b_0, c)) = \\
& (a_1 \land b_1 \land CO(a_0, b_0, c)) \lor && \text{\tiny (1)} \\
& (a_1 \land \lnot b_1 \land \lnot CO(a_0, b_0, c)) \lor && \text{\tiny (2)} \\
& (\lnot a_1 \land b_1 \land \lnot CO(a_0, b_0, c)) \lor && \text{\tiny (3)} \\
& (\lnot a_1 \land \lnot b_1 \land CO(a_0, b_0, c)) && \text{\tiny (4)} \\
&& \text{By Def. 2.1}
\end{align*}
\textbf{Subproof 1:} Expanding disjunction (1) from $S(a_1, b_1, CO(a_0, b_0, c))$:
\begin{align*}
(1) & \quad (a_1 \land b_1 \land (a_0 \land b_0) \lor (a_0 \land c) \lor (b_0 \land c) ) \\
(2) & \quad (a_1 \land a_0 \land b_1 \land b_0) \lor \\
& \quad (a_1 \land a_0 \land b_1 \land c) \lor \\
& \quad (a_1 \land b_1 \land b_0 \land c) \\
&& \text{Distrib} \\
\intertext{The resulting three disjunctions correspond to (1), (2) and (3) in $CLAS_1$}
\end{align*}
\textbf{Subproof 2:} Expanding disjunction (2) from $S(a_1, b_1, CO(a_0, b_0, c))$:
\begin{align*}
(1) & \quad (a_1 \land \lnot b_1 \land \lnot((a_0 \land b_0) \lor (a_0 \land c) \lor (b_0 \land c)) ) \\
(2) & \quad (a_1 \land \lnot b_1 \land ((\lnot a_0 \lor \lnot b_0) \land (\lnot a_0 \lor \lnot c) \land (\lnot b_0 \lor \lnot c))) && \text{De Morgan} \\ \\
& \quad \textbf{Let} \: A = \lnot a_0, B = \lnot b_0, C = \lnot c, \text{we then have:} \\ \\
& \quad (i) \: a_1 \land \lnot b_1 \land ((A \lor B) \land (A \lor C) \land (B \lor C)) \\
& \quad (ii) \: a_1 \land \lnot b_1 \land ((A \land A \land B) \lor (A \land A \land C) \lor \\
& \qquad \: (A \land C \land B) \lor (A \land C \land C) \lor (B \land A \land B) \lor \\
& \qquad \: (B \land A \land C) \lor (B \land C \land B) \lor
(B \land C \land C)) && \text{Distrib} \\
& \quad (iii) \: a_1 \land \lnot b_1 \land ((A \land B) \lor(A \land C) \lor (A \land B \land C) \lor (B \land C)) && \text{Idemp, Commut} \\
& \quad (iv) \: a_1 \land \lnot b_1 \land ((A \land B) \lor(A \land C) \lor (B \land C)) && \text{Absorp} \\
& \quad (v) \: (a_1 \land A \land \lnot b_1 \land B) \lor(a_1 \land A \land \lnot b_1 \land C) \lor (a_1 \land \lnot b_1 \land B \land C) && \text{Distrib} \\ \\
& \quad \text{After substituting, we have:} \\ \\
(3) & \quad (a_1 \land \lnot a_0 \land \lnot b_1 \land \lnot b_0) \lor \\
& \quad (a_1 \land \lnot a_0 \land \lnot b_1 \land \lnot c) \lor \\
& \quad (a_1 \land \lnot b_1 \land \lnot b_0 \land \lnot c)\\
\intertext{The resulting three disjunctions correspond to (4), (5) and (6) in $CLAS_1$}
\end{align*}
\textbf{Subproof 3:} Expanding disjunction (3): \\ \\
\indent \indent Again, we have $ \lnot CO(a_0, b_0, c) $ as we did in disjunction (2). \\
\indent \indent So, let $ A = \lnot a_0, B = \lnot b_0, C = \lnot c,$ as we did in subproof 2. \\
\indent \indent After applying the same rules, we get: \\
\begin{align*}
(1) & \quad (\lnot a_1 \land A \land b_1 \land B) \lor(\lnot a_1 \land A \land b_1 \land C) \lor (\lnot a_1 \land b_1 \land B \land C) \\
(2) & \quad (\lnot a_1 \land \lnot a_0 \land b_1 \land \lnot b_0) \lor \\
& \quad (\lnot a_1 \land \lnot a_0 \land b_1 \land \lnot c) \lor \\
& \quad (\lnot a_1 \land b_1 \land \lnot b_0 \land \lnot c) && \text{Distrib}
\intertext{The resulting three disjunctions correspond to (10), (11) and (9) in $CLAS_1$}
\end{align*}
\textbf{Subproof 4:} Expanding disjunction (4):
\begin{align*}
(1) & \quad (\lnot a_1 \land \lnot b_1 \land (a_0 \land b_0) \lor (a_0 \land c) \lor (b_0 \land c) ) \\
(2) & \quad (\lnot a_1 \land a_0 \land \lnot b_1 \land b_0) \lor \\
& \quad (\lnot a_1 \land a_0 \land \lnot b_1 \land c) \lor \\
& \quad (\lnot a_1 \land \lnot b_1 \land b_0 \land c) \\
&& \text{Distrib} \\
\intertext{The resulting three disjunctions correspond to (7), (8) and (12) in $CLAS_1$}
\end{align*}
\noindent We have showed by expanding $S(a_1, b_1, CO(a_0, b_0, c))$ that we get the exact definition of $CLAS_1(a_1, a_0, b_1, b_0, c)$. Therefore, $CLAS_1(a_1, a_0, b_1, b_0, c) \iff S(a_1, b_1, CO(a_0, b_0, c)) $
\end{proof}
\noindent \textbf{Lemma 3.3} $ (\forall a_1, a_0, b_1, b_0, c \in \{T, F\}) \; CLACO(a_1, a_0, b_1, b_0, c) \iff CO(a_1, b_1, CO(a_0, b_0, c)) $
\begin{proof}
\begin{align*}
(1) & \quad CO(a_1, b_1, CO(a_0, b_0, c)) && \text{Assump} \\
(2) & \quad (a_1 \land b_1) \lor \\
& \quad (a_1 \land ((a_0 \land b_0) \lor (a_0 \land c) \lor (b_0 \land c)) ) \lor \\
& \quad (b_1 \land ((a_0 \land b_0) \lor (a_0 \land c) \lor (b_0 \land c)))
&& \text{By Def. 2.1} \\
(3) & \quad (a_1 \land b_1) \lor \\
& \quad (a_1 \land a_0 \land b_0) \lor (a_1 \land a_0 \land c) \lor (a_1 \land b_0 \land c) \lor \\
& \quad (a_0 \land b_1 \land b_0) \lor (a_0 \land b_1 \land c) \lor (b_1 \land b_0 \land c) && \text{Distrib}
\end{align*}
This is clearly the definition of $ CLACO(a_1, a_0, b_1, b_0, c) .$\\
Therefore, $CLACO(a_1, a_0, b_1, b_0, c) \iff CO(a_1, b_1, CO(a_0, b_0, c)) $ \\
\end{proof}
\noindent \textbf{Definition 3.2} Suppose $a_n, a_{n-1}, \ldots, a_1, a_0, b_n, b_{n-1}, \ldots, b_1, b_0,$ and $c$ are propositions for any positive integer $ n $. Then, carry-out and sum outputs of an $N$-bit carry-look-ahead adder are defined as follows:
\begin{enumerate}
\item $ CLANCO(a_n, \ldots, a_0, b_n, \ldots, b_0, c) :\equiv \\
CLACO(a_n, a_{n-1}, b_n, b_{n-1}, CLACO(\ldots, CLACO(a_1, a_0, b_1, b_0, c))\ldots)$
\item $ CLANS_0(a_n, \ldots, a_0, b_n, \ldots, b_0, c) :\equiv \\
CLAS_0(a_n, b_n, CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) $
\item $ CLANS_1(a_n, \ldots, a_0, b_n, \ldots, b_0, c) :\equiv \\
CLAS_1(a_n, a_{n-1}, b_n, b_{n-1}, CLANCO(a_{n-2}, \ldots, a_0, b_{n-2}, \ldots, b_0, c)) $
\end{enumerate}
\noindent \textbf{Definition 3.3}: Suppose $a_n, \ldots, a_0, b_n, \ldots, b_0$, and $c$ are propositions and $n$ is any positive integer, then we have the following:
\begin{enumerate}
\item $ P_{CO}(n) :\equiv (\forall a_n, \ldots, a_0, b_n, \ldots, b_0, c \in \{T, F\} ) \; CLANCO(a_n, \ldots, a_0, b_n, \ldots, b_0, c) \iff CRACO(a_n, \ldots, a_0, b_n, \ldots, b_0, c) $
\item $P_{S_0}(n) :\equiv (\forall a_n, \ldots, a_0, b_n, \ldots, b_0, c \in \{T, F\} ) \; CLANS_0(a_n, \ldots, a_0, b_n, \ldots, b_0, c) \iff CRAS(a_n, \ldots, a_0, b_n, \ldots, b_0, c) $
\item $P_{S_1}(n) :\equiv (\forall a_n, \ldots, a_0, b_n, \ldots, b_0, c \in \{T, F\} ) \; CLANS_1(a_n, \ldots, a_0, b_n, \ldots, b_0, c) \iff CRAS(a_n, \ldots, a_0, b_n, \ldots, b_0, c) $
\end{enumerate}
\noindent \textbf{Lemma 3.4} For any positive integer $n$, we have $ P_{CO}(n)$
\begin{proof} We begin by proving the base case $P_{CO}(1)$, that is: \\
\textbf{Base:}
\begin{align*}
& P_{CO}(1) \equiv (\forall a_1, a_0, b_1, b_0, c \in \{T, F\} ) \; CLANCO(a_1, a_0, b_1, b_0, c) \iff \\ & \quad CRACO(a_1, a_0, b_1, b_0, c)
\end{align*}
By definition of $CLANCO$ and $CRACO$, all we really have to prove is:
\begin{align*}
& (\forall a_1, a_0, b_1, b_0, c \in \{T, F\} ) \; CLACO(a_1, a_0, b_1, b_0) \iff \\
& \quad CO(a_1, b_1, CO(a_0, b_0, c))
\end{align*}
We already proved this by Lemma 3.3 \\ \\
\textbf{Inductive Hypothesis:} Suppose $P_{CO}(n) $ is $true$ for all integers $n \geq 1$. That is, $CLANCO(a_n, \ldots, a_0, b_n, \ldots, b_0, c) \iff
\: CRACO(a_n, \ldots, a_0, b_n, \ldots, b_0, c)$ \\ \\
\textbf{Inductive Step:} We show that $P_{CO}(n+1)$ is also $true$: \\
Given our inductive hypothesis we can assume \\ \\
$ CRACO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c)$, which, by definition of 2.2 is \\ \\
$CO(a_{n+1}, b_{n+1}, CO(a_n, b_n, CO(\ldots, CO(a_0, b_0, c))\ldots)$. \\ \\
Now, from our inductive hypothesis and definition 3.2, the innermost nested \\ \\
$CO(a_n, b_n, CO(\ldots, CO(a_0, b_0, c))\ldots)$ is equivalent to \\ \\
$ CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)$, \\ \\
but we will only substitute the $n-2$ nested portion: \\ \\
$CO(a_{n+1}, b_{n+1}, CO(a_n, b_n, CLANCO(a_{n-1},
\ldots, a_0, b_{n-1}, \ldots, b_0, c)))$. \\ \\
By definition 2.1, we have: \\
\begin{align*}
& \left[a_{n+1} \land b_{n+1} \right] \lor \\
& \left[ a_{n+1} \land (a_{n} \land b_{n}) \lor \right. \\
&\qquad (a_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \lor \\
&\qquad \left. (b_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c))\right] \lor \\
& \left[ b_{n+1} \land (a_{n} \land b_{n}) \lor \right. \\
&\qquad (a_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \lor \\
&\qquad \left. (b_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \right] \\
\end{align*}
Which after distributing becomes:
\begin{align*}
& \left[a_{n+1} \land b_{n+1} \right] \lor \\
& \left[ (a_{n+1} \land a_{n} \land b_{n}) \lor \right. \\
&\qquad (a_{n+1} \land a_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \lor \\
&\qquad \left. (a_{n+1} \land b_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c))\right] \lor \\
& \left[ (a_{n} \land b_{n+1} \land b_{n}) \lor \right. \\
&\qquad (a_{n} \land b_{n+1} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \lor \\
&\qquad \left. (b_{n+1} \land b_{n} \land CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c)) \right] \\
\end{align*}
By definition 3.1, this is equivalent to: \\
\begin{align*}
& CLACO(a_{n+1}, a_n, b_{n+1}, b_n, CLANCO(a_{n-1}, \ldots, a_0, b_{n-1}, \ldots, b_0, c))
\end{align*}
which, by definiton 3.2 is:
\begin{align*}
& CLANCO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c)
\end{align*}
Since we derived the definition of $CLANCO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c) $ from $CRACO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c)$, we can conclude:
\begin{align*}
P_{CO}(n+1) \equiv CLANCO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c) \iff \\
CRACO(a_{n+1}, \ldots, a_0, b_{n+1}, \ldots, b_0, c)
\end{align*}
By induction $P_{CO}(n)$ is $true$ for all integers $n \geq 1$.
\end{proof}
\noindent \textbf{Lemma 3.5} For any positive integer $n$, we have $ P_{S_0}(n) $
\begin{proof}
\begin{align*}
\end{align*}
\end{proof}
\noindent \textbf{Lemma 3.6} For any positive integer $n$, we have $ P_{S_1}(n) $
\begin{proof}
\begin{align*}
\end{align*}
\end{proof}
\end{document}