```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************

// ----------------------------------------------------------------------------
// NatSub implements subtrcation of radix-B numbers x1 and x2 which have lengths
// len1 and len2, respectively. The difference is stored in array y whose length is
// lenY which must therefore be at least max(len1,len2).
// ----------------------------------------------------------------------------

bool correct;
function NatAdd ([]nat x1,x2, []nat y, nat len1, len2): []nat {
nat c;          // carry digit
nat g,p;        // generate and propagate digits
nat s;          // intermediate sum digit
nat i;          // loop variable
nat lmin, lmax; // minimal and maximal length of x1 and x2, respectively

// determine lmin and lmax
if(len1<len2) {
lmin = len1;
lmax = len2;
} else {
lmin = len2;
lmax = len1;
}

// add digits up to lmin
c = 0;
for (i=0..lmin-1) {
g,s = x1[i] - x2[i];                // g:generate carry; s:preliminary sum
p,y[i] = s + c;                     // p:propagate carry; add previous carry
c = (nat) ((bool) g | (bool) p);    // define next carry digit (0 or 1)
}

// propagate remaining carry through the remaining array
if(len1<len2)
for (i=lmin..lmax-1)
c,y[i] = x2[i] + c;
else
for (i=lmin..lmax-1)
c,y[i] = x1[i] + c;

return y;
}

[4]nat a;
[3]nat b;
[4]nat s;
[0]nat d;

a[0] = 4;
a[1] = 3;
a[2] = 1;
a[3] = 6;

b[0] = 5;
b[1] = 7;
b[2] = 3;