Ignore:
Timestamp:
Dec 3, 2010, 11:52:05 PM (9 years ago)
Author:
sacerdot
Message:

No more axioms! All proofs completed.
(Interrupts, I/O and timers not ported to Matita yet)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/DoTest.ma

    r369 r372  
    2828*)
    2929
     30(*
    3031nlemma xoo:
    3132 (let testfinal ≝ testfinal in
     
    3536nqed.
    3637
     38ndefinition is_JZ ≝
     39 λi: instruction.match i with
     40     [ Jump arg ⇒
     41        match arg with
     42         [ JZ arg ⇒
     43            match arg with
     44             [ RELATIVE arg ⇒ arg
     45             | _ ⇒ zero eight ]
     46         | _ ⇒ zero eight ]
     47     | _ ⇒ zero eight ].
     48
     49nlemma xoo:
     50 (let testfinal ≝ testfinal in
     51   is_JZ
     52    (first … (first … (fetch (code_memory testfinal) (program_counter testfinal))))
     53    )
     54  = zero eight.
     55 nnormalize in ⊢ (??%?);
     56
     57*)
     58
     59
    3760nlemma xoo: program_counter testfinal = program_counter testfinal.
    3861 nnormalize in ⊢ (??%?);
     62 nnormalize in ⊢ (???%);
     63 @.
    3964nqed.
Note: See TracChangeset for help on using the changeset viewer.