Changeset 2246
 Timestamp:
 Jul 24, 2012, 5:51:11 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2245 r2246 589 589 lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 Heq1 590 590 inversion instr normalize nodelta 591 [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 592 #Hi normalize in Hi; 593 cases (le_to_or_lt_eq … Hi) Hi #Hi 594 [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 595 [1,3,5: <Heq2b >lookup_insert_miss 596 [1,3,5: >lookup_insert_miss 597 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 598 *: @bitvector_of_nat_abs try assumption 599 [2,4,6: @lt_to_not_eq @Hi 600 *: @(transitive_lt ??? Hi) assumption ]] 591 [ #pi #Hins whd in match jump_expansion_step_instruction; normalize nodelta 592 lapply (destination_of_None_to_is_jump_false pi) 593 lapply (destination_of_Some_to_is_jump_true pi) 594 cases (destination_of ?) normalize nodelta 595 [ #_ #dest_None  #tgt #dest_Some #_ ]] 596 try (#x #y #Hins #Heq1 #Hold #Hadded #i #Hi) 597 try (#x #Hins #Heq1 #Hold #Hadded #i #Hi) 598 try (#Heq1 #Hold #Hadded #i #Hi) 599 >append_length in Hi; >commutative_plus #Hi normalize in Hi; 600 cases (le_to_or_lt_eq … Hi) Hi #Hi 601 [1,3,5,7,9,11,13: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 602 [1,3,5,7,9,11,13: <Heq2b >lookup_insert_miss 603 [1,3,5,7,9,11,13: >lookup_insert_miss 604 [1,3,5,7,9,11,13: 605 try @(Hold Hadded i (le_S_to_le … Hi)) 606 @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero 601 607 *: @bitvector_of_nat_abs try assumption 602 [2,4,6: @lt_to_not_eq @le_S @Hi 603 *: @(transitive_lt … Hi) assumption ]] 604 *: >Hi >lookup_insert_miss 605 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 606 @sym_eq (* USE: fst p = lookup prefix *) 607 @Hpolicy2 608 *: @bitvector_of_nat_abs try assumption 609 @lt_to_not_eq %]] 610 2,4,6: >Hi >lookup_insert_hit 611 (* USE fst p = lookup prefix *) 612 >Hpolicy2 613 <(Hold Hadded (prefix) (le_n (prefix))) 614 (* USE: sigma_compact (from old_sigma) *) 615 lapply (pi2 ?? old_sigma (prefix) ?) 616 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 617 *: 618 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 619 [1,3,5: normalize nodelta #_ #ABS cases ABS 620 *: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 621 [1,3,5: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS 622 *: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ 623 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 624 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 625 >prf >p1 >Hins >nth_append_second try % 626 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 627 #H >H @plus_left_monotone @instruction_size_irrelevant % ]]]] 628 4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 629 #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi #Hi 630 [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 631 [1,3: >lookup_insert_miss 632 [1,3: >lookup_insert_miss 633 [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; 634 @plus_zero_zero 635 2,4: @bitvector_of_nat_abs 636 [3,6: @lt_to_not_eq @Hi 637 1,4: @(transitive_lt ??? Hi) 638 ] 639 assumption 640 ] 641 2,4: @bitvector_of_nat_abs 642 [3,6: @lt_to_not_eq @le_S @Hi 643 1,4: @(transitive_lt ??? Hi) assumption] 644 assumption ] 645 2,4: >Hi >lookup_insert_miss 646 [1,3: >lookup_insert_hit >(Hold ? (prefix) (le_n (prefix))) 647 [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 608 [2,4,6,8,10,12,14: @lt_to_not_eq @Hi 609 *: @(transitive_lt ??? Hi) assumption ]] 610 *: @bitvector_of_nat_abs try assumption 611 [2,4,6,8,10,12,14: @lt_to_not_eq @le_S @Hi 612 *: @(transitive_lt … Hi) assumption ]] 613 *: >Hi >lookup_insert_miss 614 [1,3,5,7,9,11,13: >lookup_insert_hit 615 try (>(Hold Hadded (prefix) (le_n (prefix))) 616 @sym_eq (* USE: fst p = lookup prefix *) 617 @Hpolicy2) 618 >(Hold ? (prefix) (le_n (prefix))) 619 [2,4,6,8: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 648 620 (* USE: fst p = lookup prefix *) 649 @Hpolicy2 650 2,4: @bitvector_of_nat_abs try assumption 651 @lt_to_not_eq @le_n]] 652 2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1)) 653 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 654 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1)) 655 @jump_length_le_max % 656 *: #H (* USE: fst p = lookup prefix *) 657 >Hpolicy2 658 <(Hold ? (prefix) (le_n (prefix))) 659 [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H 660 >(jump_length_equal_max … H) try % 661 (* USE: sigma_compact_unsafe (from old_sigma) *) 662 lapply (pi2 ?? old_sigma (prefix) ?) 663 [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 664 2,4: inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 665 [1,3: normalize nodelta #_ #ABS cases ABS 666 2,4: normalize nodelta 667 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 668 [1,3: #_ * #pc #j normalize nodelta #_ #ABS cases ABS 669 2,4: * #Spc #Sj #EQS #x cases x x #pc #j #EQ 670 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 671 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 672 >EQpair @eq_f >prf >nth_append_second try % 673 <minus_n_n >p1 whd in match (nth ????); >Hins 674 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ' 675 >(proj2 … (pair_destruct … EQ')) % ]]] 676 2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded *: skip]]]] 677 1: #pi cases pi normalize nodelta 678 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 679 [1,2,3,6,7,24,25: #x #y 680 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 681 #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 682 cases (le_to_or_lt_eq … Hi) Hi #Hi 683 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 684 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 685 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 686 <(proj2 ?? (pair_destruct ?????? Heq2)) 687 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 i)) 688 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 689 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i) inc_sigma) 690 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 691 @(Hold Hadded i (le_S_to_le … Hi)) 692 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 693 @bitvector_of_nat_abs 694 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 695 @lt_to_not_eq @Hi 696 1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 697 @(transitive_lt ??? Hi) 698 ] 699 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 700 @le_S_S <plus_n_Sm @le_S @le_plus_n_r 701 ] 702 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 703 @bitvector_of_nat_abs 704 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 705 @lt_to_not_eq @le_S @Hi 706 1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 707 @(transitive_lt … Hi) @le_S_to_le 708 ] 709 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 710 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 711 ] 712 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 713 >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 (prefix))) 714 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 715 >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) @sym_eq 716 (* USE: fst p = lookup prefix *) 717 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 718 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 719 @bitvector_of_nat_abs 720 [3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 721 @lt_to_not_eq @le_n 722 1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 723 @le_S_to_le 724 ] 725 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 726 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 727 ] 728 ] 729 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 730 >Hi >lookup_insert_hit 731 (* USE fst p = lookup prefix *) 732 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 733 <(Hold Hadded (prefix) (le_n (prefix))) 734 (* USE: sigma_compact (from old_sigma) *) 735 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (prefix) ?) 736 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 737 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 738 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 739 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 740 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% > %); 741 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 742 normalize nodelta #_ #ABS cases ABS 743 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 744 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 745 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 746 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 747 normalize nodelta #Hl #x cases x x #pc #j normalize nodelta #Hl2 #ABS cases ABS 748 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 749 normalize nodelta #x cases x x #Spc #Sj #EQS #x cases x x #pc #j #EQ 750 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 751 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 752 >prf >p1 >Hins >nth_append_second 753 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 754 @(le_n (prefix)) 755 1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 756 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 757 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H 758 ] 759 ] 760 ] 761 ] 762 ] 763 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded 764 #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 765 Hi #Hi 766 [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 767 [1,3,5,7,9,11,13,15,17: 768 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 i)) 769 [1,3,5,7,9,11,13,15,17: 770 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i) inc_sigma) 771 [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi)) 772 >commutative_plus in Hadded; @plus_zero_zero 773 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 774 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 775 1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) 776 ] 777 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 778 >append_length @le_plus_n_r 779 ] 780 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 781 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi 782 1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le 783 ] 784 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 785 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 786 ] 787 2,4,6,8,10,12,14,16,18: >Hi 788 >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 (prefix))) 789 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (prefix) (le_n (prefix))) 790 [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 791 (* USE: fst p = lookup prefix *) 792 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 793 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 794 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n 795 1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (prefix)))) 796 ] 797 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf 798 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 799 ] 800 ] 801 2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1)) 802 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 803 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt 804 <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/ 805 2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup prefix *) 806 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 807 <(Hold ? (prefix) (le_n (prefix))) 808 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H 809 >(jump_length_equal_max … H) 810 [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *) 811 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (prefix) ?) 812 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 813 2,4,6,8,10,12,14,16,18: lapply Holdeq 814 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 815 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% → %); 816 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS 817 2,4,6,8,10,12,14,16,18: normalize nodelta 818 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 819 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 820 [1,3,5,7,9,11,13,15,17: #_ #x cases x x #pc #j normalize nodelta 821 #_ #_ #ABS cases ABS 822 2,4,6,8,10,12,14,16,18: #x cases x x #Spc #Sj #EQS #x cases x x 823 #pc #j #EQ 824 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 825 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair 826 >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second 827 [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H 828 2,4,6,8,10,12,14,16,18: @le_n 829 ] 830 ] 831 ] 832 ] 833 2,4,6,8,10,12,14,16,18: / by I/ 834 ] 835 2,4,6,8,10,12,14,16,18: @plus_zero_zero 836 [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded] 837 ] 838 ] 839 ] 840 ] 841 ] 621 @Hpolicy2 622 *: @bitvector_of_nat_abs try assumption 623 @lt_to_not_eq %]] 624 *: >Hi >lookup_insert_hit 625 (* USE fst p = lookup prefix *) 626 >Hpolicy2 627 <(Hold ? (prefix) (le_n (prefix))) try @Hadded 628 [3,7,9: @plus_zero_zero [2,4,6: >commutative_plus @Hadded *: skip]] 629 (* USE: sigma_compact (from old_sigma) *) 630 lapply (pi2 ?? old_sigma (prefix) ?) 631 [1,3,5,7,9,11,13: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 632 *: 633 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 634 [1,3,5,7,9,11,13: normalize nodelta #_ #ABS cases ABS 635 *: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 636 [1,3,5,7,9,11,13: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS 637 *: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ 638 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 639 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 640 >prf >p1 >Hins >nth_append_second try % 641 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 642 #H >H @plus_left_monotone 643 [1,3,4,7: @instruction_size_irrelevant try % 644 whd in match is_jump; normalize nodelta >dest_None % 645 *: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ' 646 >(proj2 … (pair_destruct … EQ')) 647 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 648 [1,3,5: #H @⊥ @(absurd ? H) @le_to_not_lt 649 <(proj2 ?? (pair_destruct ?????? Heq1)) 650 @jump_length_le_max try % 651 whd in match is_jump; normalize nodelta >dest_Some %] 652 #EQisize >(proj2 … (pair_destruct … Heq1)) >EQisize % ]]]]] 842 653 qed. 843 654
Note: See TracChangeset
for help on using the changeset viewer.