Changeset 1907 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 26, 2012, 5:37:21 PM (8 years ago)
Author:
mulligan
Message:

Fixes to get file to compile

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1906 r1907  
    361361
    362362(* XXX: todo *)
    363 axiom subaddressing_mode_elim:
     363lemma subaddressing_mode_elim:
    364364  ∀T: Type[2].
    365365  ∀m: nat.
     
    372372    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    373373      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
     374  #T #m #n #Q #fixed_v
     375  elim fixed_v
     376  [1:
     377    #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
     378    #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
     379    normalize
     380  |2:
     381  ]
     382  cases daemon
     383qed.
    374384
    375385definition current_instruction_is_labelled ≝
Note: See TracChangeset for help on using the changeset viewer.