Ignore:
Timestamp:
Dec 3, 2010, 4:47:03 PM (10 years ago)
Author:
mulligan
Message:

Most of critical lemma done. Hole remaining that I can't coax matita into solving.

File:
1 edited

Legend:

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

    r367 r370  
    9292   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
    9393
    94 nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
    95  match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
    96   [ Empty ⇒ λK.⊥
    97   | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
    98      match m return λz.m = z → Bool with
    99       [ Z ⇒ λ_.is_a he A
    100       | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
    101 (* CSC: cast not working here: why? *)
    102 ##[##4: #x; ncases K; napply x ]
    103 //; ndestruct.
    104 nqed.
     94
     95nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝
     96 match l return λm.λ_:Vector addressing_mode_tag m.Bool with
     97  [ Empty ⇒ false
     98  | Cons m he (tl: Vector addressing_mode_tag m) ⇒
     99     is_a he A ∨ is_in ? tl A ].
    105100
    106101ndefinition bool_to_Prop ≝
Note: See TracChangeset for help on using the changeset viewer.