helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
  20
  21 (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *)
  22
  23 (*#* printing sqrt_I %\ensuremath{\sqrt{\imath}}% *)
  24
  25 (*#* printing nroot_I %\ensuremath{\sqrt[n]{\imath}}% *)
  26
  27 (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
  28
  29 include "complex/CComplex.ma".
  30
  31 (*#* * Roots of Complex Numbers
  32
  33 Properties of non-zero complex numbers
  34 *)
  35
  36 (* UNEXPORTED
  37 Section CC_ap_zero
  38 *)
  39
  40 inline procedural "cic:/CoRN/complex/NRootCC/cc_ap_zero.con".
  41
  42 inline procedural "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con".
  43
  44 (* UNEXPORTED
  45 End CC_ap_zero
  46 *)
  47
  48 (*#* Weird lemma. *)
  49
  50 (* UNEXPORTED
  51 Section Imag_to_Real
  52 *)
  53
  54 inline procedural "cic:/CoRN/complex/NRootCC/imag_to_real.con".
  55
  56 (* UNEXPORTED
  57 End Imag_to_Real
  58 *)
  59
  60 (*#* ** Roots of the imaginary unit *)
  61
  62 (* UNEXPORTED
  63 Section NRootI
  64 *)
  65
  66 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_Half.con".
  67
  68 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I.con".
  69
  70 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con".
  71
  72 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con".
  73
  74 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I.con".
  75
  76 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con".
  77
  78 (* UNEXPORTED
  79 Hint Resolve nroot_I_nexp: algebra.
  80 *)
  81
  82 inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I.con".
  83
  84 inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con".
  85
  86 (* UNEXPORTED
  87 End NRootI
  88 *)
  89
  90 (*#* ** Roots of complex numbers *)
  91
  92 (* UNEXPORTED
  93 Section NRootCC_1
  94 *)
  95
  96 (*#* We define the nth root of a complex number with a non zero imaginary part.
  97 *)
  98
  99 (* UNEXPORTED
 100 Section NRootCC_1_ap_real
 101 *)
 102
 103 (*#*
 104 %\begin{convention}% Let [a,b : IR] and [b_ : (b [#] Zero)].
 105 Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
 106 [a' := sqrt a'2], [b'2 := (c[-]a) [*]Half] and [b' := sqrt b'2].
 107 %\end{convention}%
 108 *)
 109
 110 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var".
 111
 112 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var".
 113
 114 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var".
 115
 116 (* begin hide *)
 117
 118 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__".
 119
 120 (* end hide *)
 121
 122 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con".
 123
 124 (* begin hide *)
 125
 126 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__".
 127
 128 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__".
 129
 130 (* end hide *)
 131
 132 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con".
 133
 134 (* begin hide *)
 135
 136 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__".
 137
 138 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__".
 139
 140 (* end hide *)
 141
 142 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con".
 143
 144 (* begin hide *)
 145
 146 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__".
 147
 148 (* end hide *)
 149
 150 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a3.con".
 151
 152 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a4.con".
 153
 154 (* UNEXPORTED
 155 Hint Resolve nrCC1_a4: algebra.
 156 *)
 157
 158 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a5.con".
 159
 160 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6.con".
 161
 162 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con".
 163
 164 (* UNEXPORTED
 165 Hint Resolve nrCC1_a5: algebra.
 166 *)
 167
 168 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con".
 169
 170 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con".
 171
 172 (* UNEXPORTED
 173 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
 174 *)
 175
 176 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con".
 177
 178 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con".
 179
 180 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con".
 181
 182 (* UNEXPORTED
 183 End NRootCC_1_ap_real
 184 *)
 185
 186 (*#* We now define the nth root of a complex number with a non zero real part.
 187 *)
 188
 189 (* UNEXPORTED
 190 Section NRootCC_1_ap_imag
 191 *)
 192
 193 (*#*
 194 %\begin{convention}% Let [a,b : IR] and [a_ : (a [#] Zero)] and define
 195 [c' := (a[+I*]b) [*][--]II := a'[+I*]b'].
 196 %\end{convention}%
 197 *)
 198
 199 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var".
 200
 201 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var".
 202
 203 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var".
 204
 205 (* begin hide *)
 206
 207 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 208
 209 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 210
 211 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 212
 213 (* end hide *)
 214
 215 (* UNEXPORTED
 216 Hint Resolve sqrt_I_nexp: algebra.
 217 *)
 218
 219 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con".
 220
 221 (* UNEXPORTED
 222 End NRootCC_1_ap_imag
 223 *)
 224
 225 (*#* We now define the roots of arbitrary non zero complex numbers. *)
 226
 227 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1.con".
 228
 229 (* UNEXPORTED
 230 End NRootCC_1
 231 *)
 232
 233 (* UNEXPORTED
 234 Section NRootCC_2
 235 *)
 236
 237 (*#*
 238 %\begin{convention}% Let [n : nat] and [c,z : CC] and [c_:(c [#] Zero)].
 239 %\end{convention}%
 240 *)
 241
 242 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_2/n.var".
 243
 244 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c.var".
 245
 246 alias id "z" = "cic:/CoRN/complex/NRootCC/NRootCC_2/z.var".
 247
 248 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var".
 249
 250 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2'.con".
 251
 252 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2.con".
 253
 254 (* UNEXPORTED
 255 End NRootCC_2
 256 *)
 257
 258 (* UNEXPORTED
 259 Section NRootCC_3
 260 *)
 261
 262 inline procedural "cic:/CoRN/complex/NRootCC/Im_poly.con".
 263
 264 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a1.con".
 265
 266 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a2.con".
 267
 268 (*#*
 269 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
 270 %\end{convention}%
 271 *)
 272
 273 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_3/a.var".
 274
 275 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b.var".
 276
 277 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var".
 278
 279 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3/n.var".
 280
 281 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con".
 282
 283 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a3.con".
 284
 285 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a4.con".
 286
 287 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a5.con".
 288
 289 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a6.con".
 290
 291 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con".
 292
 293 (* UNEXPORTED
 294 Hint Resolve nrCC3_a3: algebra.
 295 *)
 296
 297 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a7.con".
 298
 299 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a8.con".
 300
 301 (* UNEXPORTED
 302 Hint Resolve nth_coeff_p_mult_c_: algebra.
 303 *)
 304
 305 (* UNEXPORTED
 306 Hint Resolve nrCC3_a6: algebra.
 307 *)
 308
 309 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a9.con".
 310
 311 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con".
 312
 313 (* UNEXPORTED
 314 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
 315 *)
 316
 317 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_.con".
 318
 319 (* UNEXPORTED
 320 Hint Resolve nrootCC_3_: algebra.
 321 *)
 322
 323 (* UNEXPORTED
 324 Hint Resolve calculate_Im: algebra.
 325 *)
 326
 327 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3.con".
 328
 329 (* UNEXPORTED
 330 Hint Resolve nrCC3_a2: algebra.
 331 *)
 332
 333 (* UNEXPORTED
 334 Hint Resolve nrCC3_a9: algebra.
 335 *)
 336
 337 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con".
 338
 339 (* UNEXPORTED
 340 End NRootCC_3
 341 *)
 342
 343 (* UNEXPORTED
 344 Section NRootCC_3'
 345 *)
 346
 347 (*#*
 348 %\begin{convention}% Let [c:IR], [n:nat] and [n_:(lt (0) n)].
 349 %\end{convention}%
 350 *)
 351
 352 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var".
 353
 354 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var".
 355
 356 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var".
 357
 358 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con".
 359
 360 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'.con".
 361
 362 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con".
 363
 364 (* UNEXPORTED
 365 End NRootCC_3'
 366 *)
 367
 368 (* UNEXPORTED
 369 Section NRootCC_4
 370 *)
 371
 372 (* UNEXPORTED
 373 Section NRootCC_4_ap_real
 374 *)
 375
 376 (*#*
 377 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)], [n : nat] and
 378 [n_:(odd n)]; define [c := a[+I*]b].
 379 %\end{convention}%
 380 *)
 381
 382 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var".
 383
 384 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var".
 385
 386 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var".
 387
 388 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var".
 389
 390 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var".
 391
 392 (* begin hide *)
 393
 394 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__".
 395
 396 (* end hide *)
 397
 398 (* UNEXPORTED
 399 Section NRootCC_4_solutions
 400 *)
 401
 402 (* UNEXPORTED
 403 Hint Resolve nrootCC_3: algebra.
 404 *)
 405
 406 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1.con".
 407
 408 (*#*
 409 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
 410 %\end{convention}%
 411 *)
 412
 413 alias id "r2'" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var".
 414
 415 alias id "c2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var".
 416
 417 alias id "r2'_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var".
 418
 419 (* UNEXPORTED
 420 Hint Resolve nrootCC_3': algebra.
 421 *)
 422
 423 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con".
 424
 425 (* UNEXPORTED
 426 End NRootCC_4_solutions
 427 *)
 428
 429 (* UNEXPORTED
 430 Section NRootCC_4_equations
 431 *)
 432
 433 (*#*
 434 %\begin{convention}% Let [r,y2 : IR] be such that
 435 [(r[+I*]One) [^]n[*] (CC_conj c) [-] (r[+I*][--]One) [^]n[*]c [=] Zero]
 436 and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
 437 %\end{convention}%
 438 *)
 439
 440 alias id "r" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var".
 441
 442 alias id "r_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var".
 443
 444 alias id "y2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var".
 445
 446 alias id "y2_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var".
 447
 448 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a2.con".
 449
 450 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a3.con".
 451
 452 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a4.con".
 453
 454 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_y.con".
 455
 456 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 457
 458 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_x.con".
 459
 460 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 461
 462 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a5.con".
 463
 464 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a6.con".
 465
 466 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_z.con".
 467
 468 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 469
 470 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a7.con".
 471
 472 (* UNEXPORTED
 473 Hint Resolve nrCC4_a6: algebra.
 474 *)
 475
 476 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a8.con".
 477
 478 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a9.con".
 479
 480 (* UNEXPORTED
 481 End NRootCC_4_equations
 482 *)
 483
 484 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a10.con".
 485
 486 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con".
 487
 488 (* UNEXPORTED
 489 End NRootCC_4_ap_real
 490 *)
 491
 492 (* UNEXPORTED
 493 Section NRootCC_4_ap_imag
 494 *)
 495
 496 (*#*
 497 %\begin{convention}% Let [a,b : IR] and [n : nat] with [a [#] Zero]
 498 and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
 499 %\end{convention}%
 500 *)
 501
 502 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var".
 503
 504 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var".
 505
 506 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var".
 507
 508 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var".
 509
 510 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var".
 511
 512 (* begin hide *)
 513
 514 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 515
 516 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 517
 518 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 519
 520 (* end hide *)
 521
 522 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con".
 523
 524 (* UNEXPORTED
 525 Hint Resolve nroot_minus_I_nexp: algebra.
 526 *)
 527
 528 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con".
 529
 530 (* UNEXPORTED
 531 End NRootCC_4_ap_imag
 532 *)
 533
 534 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4.con".
 535
 536 (* UNEXPORTED
 537 End NRootCC_4
 538 *)
 539
 540 (*#* Finally, the general definition of nth root. *)
 541
 542 (* UNEXPORTED
 543 Section NRootCC_5
 544 *)
 545
 546 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a2.con".
 547
 548 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a3.con".
 549
 550 (* UNEXPORTED
 551 Hint Resolve nrCC_5a3: algebra.
 552 *)
 553
 554 (*#*
 555 %\begin{convention}% Let [c : CC] with [c [#] Zero].
 556 %\end{convention}%
 557 *)
 558
 559 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c.var".
 560
 561 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var".
 562
 563 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a4.con".
 564
 565 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_5.con".
 566
 567 (* UNEXPORTED
 568 End NRootCC_5
 569 *)
 570
 571 (*#* Final definition *)
 572
 573 inline procedural "cic:/CoRN/complex/NRootCC/CnrootCC.con".
 574