Changeset 1635 for src/common/Graphs.ma
 Timestamp:
 Jan 7, 2012, 12:33:17 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Graphs.ma
r1515 r1635 36 36 lookup ? ? (add ? ? g l s) l ≠ None ?. 37 37 38 axiom graph_add_eq: 39 ∀A: Type[0]. 40 ∀g: graph A. 41 ∀l: label. 42 ∀s: A. 43 lookup ? ? (add ? ? g l s) l = Some ? s. 44 38 45 axiom graph_add_lookup: 39 46 ∀A: Type[0]. … … 43 50 ∀to_insert: label. 44 51 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. 52 53 axiom graph_add_preserve : 54 ∀A: Type[0]. 55 ∀g: graph A. 56 ∀l: label. 57 ∀s: A. 58 ∀to_insert: label. 59 l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l. 45 60 46 61 axiom graph_num_nodes:
Note: See TracChangeset
for help on using the changeset viewer.