Ignore:
Timestamp:
Nov 29, 2010, 2:08:52 PM (9 years ago)
Author:
mulligan
Message:

Fixed segmentation fault in Nat.ma, added get_index and renamed previous get_index to get_index_weak in List.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Nat.ma

    r329 r330  
    209209
    210210(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    211 (* Lemmas.                                                                    *)
    212 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     211(* Axioms.                                                                    *)
     212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     213
     214naxiom plus_minus_inverse_left:
     215  ∀m, n: Nat.
     216    (m + n) - n = m.
     217   
     218naxiom less_than_or_equal_monotone:
     219  ∀m, n: Nat.
     220    m ≤ n → (S m) ≤ (S n).
     221   
     222naxiom succ_less_than_or_equal_injective:
     223  ∀m, n: Nat.
     224    (S m) ≤ (S n) → m ≤ n.
     225   
     226naxiom plus_minus_inverse_right:
     227  ∀m, n: Nat.
     228    (m - n) + n = m.
     229
     230naxiom greater_than_b: Nat → Nat → Bool.
    213231
    214232naxiom succ_less_than_injective:
     
    219237  ∀m: Nat.
    220238    ¬(m < Z).
     239   
     240(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     241(* Lemmas.                                                                    *)
     242(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    221243   
    222244nlemma less_than_or_equal_zero:
     
    347369  nnormalize.
    348370  nrewrite > H.
    349   napplyS succ_plus.
     371  napply succ_plus.
    350372nqed.
    351373
Note: See TracChangeset for help on using the changeset viewer.