Ignore:
Timestamp:
Aug 10, 2011, 5:17:58 PM (9 years ago)
Author:
campbell
Message:

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1102 r1105  
    1717#h #t #IH * /3/
    1818qed.
     19
     20lemma All_nth : ∀A,P,n,l.
     21  All A P l →
     22  ∀a.
     23  nth_opt A n l = Some A a →
     24  P a.
     25#A #P #n elim n
     26[ * [ #_ #a #E whd in E:(??%?); destruct
     27    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
     28    ]
     29| #m #IH *
     30  [ #_ #a #E whd in E:(??%?); destruct
     31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
     32  ]
     33] qed.
    1934
    2035let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
Note: See TracChangeset for help on using the changeset viewer.