Changeset 894
 Timestamp:
 Jun 8, 2011, 10:09:06 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r893 r894 684 684 ∀pc. 685 685 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))). 686 *) 686 687 687 axiom bitvector_elim_complete: 688 688 ∀n,P. bitvector_elim n P = true → ∀bv. P bv. … … 693 693 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ // 694 694 qed. 695 *) 696 697 698 695 699 696 700 (* … … 711 715 712 716 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. 717 718 axiom bitvector_3_elim_prop: 719 ∀P: BitVector 3 → Prop. 720 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → 721 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → 722 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 713 723 714 724 lemma test: … … 735 745 normalize in ⊢ (???% → ?) 736 746 [42,93,95: @split_elim #vl #vm #E >E E; normalize in ⊢ (???% → ?) 737 92,94: cases daemon ] 747 92,94: @split_elim #v1 #v2 #E >E E; @(bitvector_3_elim_prop … v1) normalize in ⊢ (???% → ?) 748 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2) 749 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4 750 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??) 751 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?) 752 <H2 whd BUGHERE 753 ] 738 754 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2) 739 755 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
Note: See TracChangeset
for help on using the changeset viewer.