Changeset 1035 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 22, 2011, 11:06:43 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1015 r1035 1979 1979 SFR_SP sp2) 1980 1980 pbu)). 1981 1982 theorem main_thm: 1983 ∀M,M',ps,pol. 1984 next_internal_pseudo_address_map M ps = Some … M' → 1985 ∃n. 1986 execute n (status_of_pseudo_status M ps pol) 1987 = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?. 1988 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 1989 #M #M' #ps #pol #SAFE 1990 cut 1991 (∀ps'. 1992 ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps. 1993 ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?) 1994 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))] 1995 #ps' #EQ 1996 whd in ⊢ (??(λ_.??(??%)?)) 1997 change with 1998 (∃n. 1999 execute n 2000 (set_low_internal_ram ? 2001 (set_high_internal_ram ? 2002 (set_program_counter ? 2003 (set_code_memory ?? ps (load_code_memory ?)) 2004 (sigma ? pol (program_counter ? ps))) 2005 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2006 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2007 = set_low_internal_ram ? 2008 (set_high_internal_ram ? 2009 (set_program_counter ? 2010 (set_code_memory ?? ? (load_code_memory ?)) 2011 (sigma ???)) ?) ?) 2012 >EQ whd in match eq_rect_Type0_r normalize nodelta 2013 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta 2014 generalize in match EQ -EQ; 2015 generalize in match (refl … (code_memory pseudo_assembly_program ps)) 2016 generalize in match pol generalize in ⊢ (∀_.??%? → ?) 2017 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps' 2018 2019 1981 2020 1982 2021 lemma main_thm0:
Note: See TracChangeset
for help on using the changeset viewer.