-
-
-
-
-
- change with (tick (tick (tick mult_status)) = mult_status);
- change with (tick (tick mult_status) = mult_status);
- change with (tick mult_status = mult_status);
- change with (mult_status = mult_status);
- reflexivity.
-qed.
-
-(*
- unfold mult_status;
- simplify;
- whd in ⊢ (? ?
-(?
- (?
- (?
- match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ?
- with
- [true\rArr ?|false\rArr ?]))) ?);
- simplify;
- whd in ⊢ (? ?
-(?
- (?
- (?
- match % in opcode return ? with
- [ADDd\rArr ?
- |BEQ\rArr ?
- |BRA\rArr ?
- |DECd\rArr ?
- |LDAi\rArr ?
- |LDAd\rArr ?
- |STAd\rArr ?]))) ?);
- simplify;
- whd in \vdash (? ?
-(?
- (?
- match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with
- [true\rArr ?|false\rArr ?])) ?);
- simplify;
- whd in \vdash (? ?
-(?
- (?
- match % in opcode return ? with
- [ADDd\rArr ?
- |BEQ\rArr ?
- |BRA\rArr ?
- |DECd\rArr ?
- |LDAi\rArr ?
- |LDAd\rArr ?
- |STAd\rArr ?])) ?);
- simplify;
- whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?);
- simplify;
- whd in \vdash (? ?
-(?
- match % in opcode return ? with
- [ADDd\rArr ?
- |BEQ\rArr ?
- |BRA\rArr ?
- |DECd\rArr ?
- |LDAi\rArr ?
- |LDAd\rArr ?
- |STAd\rArr ?]) ?);
- simplify;
- whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?);
- simplify;
- whd in \vdash (? ?
-match % in opcode return ? with
-[ADDd\rArr ?
-|BEQ\rArr ?
-|BRA\rArr ?
-|DECd\rArr ?
-|LDAi\rArr ?
-|LDAd\rArr ?
-|STAd\rArr ?] ?);
- simplify;
- reflexivity.
-*)
-*)
\ No newline at end of file
+lemma goo: True.
+ letin s0 ≝ mult_status;
+ letin pc0 ≝ (pc s0);
+
+ reduce in pc0;
+ letin i0 ≝ (opcode_of_byte (mem s0 pc0));
+ reduce in i0;
+
+ letin s1 ≝ (execute s0 (cycles_of_opcode i0));
+ letin pc1 ≝ (pc s1);
+ reduce in pc1;
+ letin i1 ≝ (opcode_of_byte (mem s1 pc1));
+ reduce in i1;
+
+ letin s2 ≝ (execute s1 (cycles_of_opcode i1));
+ letin pc2 ≝ (pc s2);
+ reduce in pc2;
+ letin i2 ≝ (opcode_of_byte (mem s2 pc2));
+ reduce in i2;
+
+ letin s3 ≝ (execute s2 (cycles_of_opcode i2));
+ letin pc3 ≝ (pc s3);
+ reduce in pc3;
+ letin i3 ≝ (opcode_of_byte (mem s3 pc3));
+ reduce in i3;
+
+ letin s4 ≝ (execute s3 (cycles_of_opcode i3));
+ letin pc4 ≝ (pc s4);
+ reduce in pc4;
+ letin i4 ≝ (opcode_of_byte (mem s4 pc4));
+ reduce in i4;
+
+ exact I.
+qed.
\ No newline at end of file