Ignore:
Timestamp:
Jun 27, 2012, 7:14:32 PM (9 years ago)
Author:
mulligan
Message:

Large changes from today trying to complete the main theorem. Again :(

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2124 r2129  
    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  (*
    402404  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    403405  #costs #create_label_cost_refl #newppc
    … …  
    13711373  (* XXX: finally, prove the equality using sigma commutation *)
    13721374  cases daemon
    1373   ]
    1374 qed.
     1375  ] *)
     1376qed.
Note: See TracChangeset for help on using the changeset viewer.