Changeset 1887 for src

Timestamp:

Apr 12, 2012, 1:53:38 PM (9 years ago)

Author:

boender

Message:

• added SEFM2012 directory
• some progress in assembly

Location:

src/ASM

Files:

• Assembly.ma (modified) (2 diffs)
• SEFM2012 (added)

src/ASM/Assembly.ma

@@ -846 +846 @@
      bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
  #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl
- whd in match (sigma ???); whd in match (sigma_safe ??); normalize nodelta
- lapply (pi2 ?? (
-   sigma00 pol (\snd program)
-    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉))
- normalize nodelta
+ whd in match (sigma ???); whd in match (sigma program pol (\snd (half_add ???)));
+ whd in match (sigma_safe program pol); whd in match (sigma0 program pol);
+ lapply (refl ? (pi1 ?? (sigma00 pol (\snd program)
+  «〈0, 〈0, (insert (BitVector 16) 16 (bitvector_of_nat 16 0) (bitvector_of_nat 16 0) (Stub (BitVector 16) 16))〉〉,?»)))
  [ @conj
    [ / by refl/
@@ -858 +857 @@
      ]
    ]
- |
- 
- whd in match (sigma0 program pol);
-(* here we go *)
-cases daemon
+ | (* here we go *) cases daemon
+ ] 
 qed.