Ignore:
Timestamp:
Nov 22, 2010, 11:12:56 AM (9 years ago)
Author:
mulligan
Message:

Changes to get directory to compile.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/Nat.ma

    r246 r247  
    311311  //.
    312312  #N H.
    313   //.
     313  nnormalize.
     314  nrewrite < H.
     315  @.
    314316nqed.
    315317
    … …  
    355357  #N H.
    356358  nnormalize.
    357   //.
     359  nrewrite > H.
     360  nrewrite < (plus_associative n N ?).
     361  nrewrite > (plus_symmetrical n N).
     362  nrewrite > (plus_associative N n ?).
     363  @.
    358364nqed.
    359365
    … …  
    374380  nnormalize.
    375381  nrewrite > H.
    376   napplyS multiplication_succ.
     382  nrewrite > (multiplication_succ ? ?).
     383  @.
    377384nqed.
    378385
    … …  
    386393  #N H.
    387394  nnormalize.
    388   //.
     395  nrewrite > (succ_plus ? ?).
     396  nrewrite < (succ_plus_succ_zero ?).
     397  @.
    389398nqed.
    390399
    … …  
    412421  nnormalize.
    413422  nrewrite > H.
    414   napplyS plus_associative.
     423  nrewrite < (plus_associative ? ? ?).
     424  @.
    415425nqed.
    416426
    … …  
    419429    o * (m + n) = o * m + o * n.
    420430  #m n o.
    421   napplyS multiplication_symmetrical.
     431  nelim o.
     432  //.
     433  #N H.
     434  nnormalize.
     435  nrewrite > H.
     436  nrewrite < (plus_associative ? n (N * n)).
     437  nrewrite > (plus_symmetrical (m + N * m) n).
     438  nrewrite < (plus_associative n m (N * m)).
     439  nrewrite < (plus_symmetrical n m).
     440  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
     441  @.
    422442nqed.
    423443
    … …  
    432452  nnormalize.
    433453  nrewrite > H.
    434   napplyS multiplication_distributes_right_plus.
     454  nrewrite > (multiplication_distributes_right_plus ? ? ?).
     455  @.
    435456nqed.
    436457
Note: See TracChangeset for help on using the changeset viewer.