source: Deliverables/D4.1/Matita/DoTest.ma @ 357

include "Test.ma".
include "Interpret.ma".

ndefinition testmem ≝ assembly test.
ndefinition teststatus ≝ load testmem initialise_status.
ndefinition testfinal ≝ execute one teststatus.

notation "'STATUS'" with precedence 90 for @{ 'status }.
interpretation "status" 'status = (mk_Status ??????????).

(*
nlemma xoo: testfinal = testfinal.
 nnormalize in ⊢ (??%?); @;
nqed.
*)

(*
nlemma test:
 (let status ≝
 load
  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
   initialise_status
  in
   fetch (code_memory status) (program_counter status)
  ) = ?.
##[ nnormalize in ⊢ (??%?);
*)


nlemma xoo:
 fetch (code_memory testfinal) (program_counter testfinal) =
 fetch (code_memory testfinal) (program_counter testfinal).
 nnormalize in ⊢ (??%?); @;
nqed.
*)

nlemma xoo: program_counter testfinal = program_counter testfinal.
 nnormalize in ⊢ (??%?); @;
nqed.