Changeset 2129 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jun 27, 2012, 7:14:32 PM (8 years ago)

Author:

mulligan

Message:

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

File:

• src/ASM/AssemblyProofSplit.ma (modified) (2 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -400 +400 @@
                       status_of_pseudo_status M' cm s sigma policy).
     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
+  cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *)
+  (*
   #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
   #costs #create_label_cost_refl #newppc
@@ -1371 +1373 @@
   (* XXX: finally, prove the equality using sigma commutation *)
   cases daemon
-  ]
-qed.
+  ] *)
+qed.