Ignore:
Timestamp:
Jun 28, 2012, 12:55:05 AM (8 years ago)
Author:
sacerdot
Message:

No more need for functional extensionality.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2129 r2131  
    379379  ∀newppc: Word.
    380380  ∀lookup_labels: Identifier → Word.
    381   ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
     381  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
    382382  ∀lookup_datalabels: Identifier → Word.
    383383  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
     
    400400                      status_of_pseudo_status M' cm s sigma policy).
    401401    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    402   cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *)
    403   (*
    404402  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    405403  #costs #create_label_cost_refl #newppc
     
    13731371  (* XXX: finally, prove the equality using sigma commutation *)
    13741372  cases daemon
    1375   ] *)
    1376 qed.
     1373  ]
     1374qed.
Note: See TracChangeset for help on using the changeset viewer.