Ignore:
Timestamp:
May 21, 2012, 5:48:43 PM (7 years ago)
Author:
mulligan
Message:

Work from today on closing main_thm.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1972 r1975  
    13801380  -assm #c #assm cases assm
    13811381  -assm #r #assm cases assm destruct
    1382   cases l cases c cases r //
     1382  cases l cases c cases r assumption
    13831383qed.
    13841384
     
    14511451qed.
    14521452
    1453 axiom eq_instruction_to_eq:
     1453lemma eq_instruction_to_eq:
    14541454  ∀i1, i2: instruction.
    14551455    eq_instruction i1 i2 = true → i1 ≃ i2.
     1456  #i1 #i2
     1457  cases i1 cases i2 cases daemon (*
     1458  [1,10,19,28,37,46:
     1459    #arg1 #arg2
     1460    whd in match (eq_instruction ??);
     1461    cases arg1 #subaddressing_mode
     1462    cases subaddressing_mode
     1463    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1464    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1465    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1466    #word11 #irrelevant
     1467    cases arg2 #subaddressing_mode
     1468    cases subaddressing_mode
     1469    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1470    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1471    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1472    #word11' #irrelevant normalize nodelta
     1473    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
     1474qed.
    14561475         
    14571476lemma fetch_assembly_pseudo':
Note: See TracChangeset for help on using the changeset viewer.