Ignore:
Timestamp:
Dec 3, 2010, 10:33:48 AM (9 years ago)
Author:
mulligan
Message:

Proof of missing lemma seems to be done, but won't Qed. My version of autotac seems to be behaving very strangely.

File:
1 edited

Legend:

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

    r368 r369  
    66    zero eight @@ b.
    77   
    8 naxiom execute_1_technical:
     8nlemma execute_1_technical:
    99  ∀n,m: Nat.
    1010  ∀v: Vector addressing_mode_tag (S n).
     
    1414    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    1515    bool_to_Prop (is_in ? q a).
     16  #n m v q a.
     17  nelim v.
     18  nnormalize.
     19  #H1 H2.
     20  ncases (is_in m q a).
     21  nnormalize.
     22  napply I.
     23  nnormalize.
     24  //.
     25  #N H V IH H1 H2.
     26  nnormalize.
     27  ncases (is_in m q a).
     28  nnormalize.
     29  napply I.
     30  nnormalize.
     31  //.
     32nqed.
    1633   
    1734ndefinition execute_1: Status → Status ≝
     
    500517    );
    501518    ntry (
    502       nnormalize
    503       //
    504     );
    505     ntry (
    506519      napply (execute_1_technical … (subaddressing_modein …))
    507520      napply I
    508     );     
     521    );
     522    ntry (
     523      nnormalize
     524      napply I
     525    );     
    509526nqed.
    510527
Note: See TracChangeset for help on using the changeset viewer.