Changeset 1882 for src/common/Graphs.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Graphs.ma
r1635 r1882 59 59 l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l. 60 60 61 axiom graph_num_nodes: 62 ∀A: Type[0]. 63 ∀g: graph A. 64 nat. 61 definition graph_num_nodes: 62 ∀A: Type[0].graph A → ℕ ≝ λA,g.g. 63 64 lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop. 65 (∀g.(∀g'.g'<g → P g') → P g) → ∀g.P g. 66 #A#P#H#g 67 lapply (refl ? (g)) 68 generalize in ⊢(???%→?); 69 #n lapply g g 70 @(nat_elim1 … n) 71 #m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …)) 72 qed.
Note: See TracChangeset
for help on using the changeset viewer.