helm/EXPORT/exportprove/prove/provastruct2.v

   1 Section init.
   2 Section a.
   3  Section a1.
   4   Section a11.
   5    Section a111.
   6     Local uno := (S O).
   7    End a111.
   8    Section a112.
   9    End a112.
  10    Section a113.
  11    End a113.
  12   End a11.
  13   Local uno := (S O).
  14  End a1.
  15  Section a2.
  16   Section a21.
  17    Local uno := (S O).
  18   End a21.
  19   Section a22.
  20    Section a221.
  21    End a221.
  22   End a22.
  23   Section a23.
  24    Section a231.
  25     Section a2311.
  26      Local uno := (S O).
  27     End a2311.
  28     Section a2312.
  29     End a2312.
  30     Section a2313.
  31     End a2313.
  32    End a231.
  33    Section a232.
  34     Section a2321.
  35     End a2321.
  36    End a232.
  37   End a23.
  38   Local uno := (S O).
  39  End a2.
  40  Definition uno := (S O).
  41 End a.
  42 End init.