Changeset 1887


Ignore:
Timestamp:
Apr 12, 2012, 1:53:38 PM (8 years ago)
Author:
boender
Message:
  • added SEFM2012 directory
  • some progress in assembly
Location:
src/ASM
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1885 r1887  
    846846     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    847847 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl
    848  whd in match (sigma ???); whd in match (sigma_safe ??); normalize nodelta
    849  lapply (pi2 ?? (
    850    sigma00 pol (\snd program)
    851     〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉))
    852  normalize nodelta
     848 whd in match (sigma ???); whd in match (sigma program pol (\snd (half_add ???)));
     849 whd in match (sigma_safe program pol); whd in match (sigma0 program pol);
     850 lapply (refl ? (pi1 ?? (sigma00 pol (\snd program)
     851  «〈0, 〈0, (insert (BitVector 16) 16 (bitvector_of_nat 16 0) (bitvector_of_nat 16 0) (Stub (BitVector 16) 16))〉〉,?»)))
    853852 [ @conj
    854853   [ / by refl/
     
    858857     ]
    859858   ]
    860  |
    861  
    862  whd in match (sigma0 program pol);
    863 (* here we go *)
    864 cases daemon
     859 | (* here we go *) cases daemon
     860 ]
    865861qed.
    866862 
Note: See TracChangeset for help on using the changeset viewer.