Changeset 2301 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Aug 22, 2012, 5:30:56 PM (8 years ago)
- File:
-
- 1 edited
-
src/ASM/AssemblyProofSplit.ma (modified) (60 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2285 r2301 591 591 @set_arg_8_status_of_pseudo_status try % 592 592 @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)] 593 | (*3: (* SUBB *)593 |3: (* SUBB *) 594 594 (* XXX: work on the right hand side *) 595 595 (* XXX: switch to the left hand side *) … … 597 597 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 598 598 whd in maps_assm:(??%%); 599 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1599 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 600 600 [2,4: normalize nodelta #absurd destruct(absurd) ] 601 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_2601 inversion (assert_data ?????) #addressing_mode_ok_assm_2 602 602 [2,4: normalize nodelta #absurd destruct(absurd) ] 603 603 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 611 611 [1: 612 612 @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl 613 @(get_arg_8_status_of_pseudo_status cm status … M')614 [1: 615 >status_refl @s ym_eq @set_clock_status_of_pseudo_status %613 @(get_arg_8_status_of_pseudo_status cm status … 〈low, high, accA〉) 614 [1: 615 >status_refl @set_clock_status_of_pseudo_status % 616 616 |2: 617 617 >status_refl … … 625 625 |2: 626 626 @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl 627 @(get_arg_8_status_of_pseudo_status cm status … M')628 [1: 629 >status_refl @s ym_eq @set_clock_status_of_pseudo_status %627 @(get_arg_8_status_of_pseudo_status cm status … 〈low, high, accA〉) 628 [1: 629 >status_refl @set_clock_status_of_pseudo_status % 630 630 |2: 631 631 >status_refl … … 638 638 ] 639 639 |3: 640 @(get_cy_flag_status_of_pseudo_status … M')641 @s ym_eq @set_clock_status_of_pseudo_status642 [1: 643 @s ym_eq @set_program_counter_status_of_pseudo_status %640 @(get_cy_flag_status_of_pseudo_status … 〈low, high, accA〉) 641 @set_clock_status_of_pseudo_status 642 [1: 643 @set_program_counter_status_of_pseudo_status % 644 644 |2: 645 645 % … … 653 653 |2: 654 654 @set_flags_status_of_pseudo_status try % 655 @ sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))656 [1: 657 @s ym_eq @set_clock_status_of_pseudo_status %655 @(set_arg_8_status_of_pseudo_status … (refl …)) 656 [1: 657 @set_clock_status_of_pseudo_status % 658 658 |2: 659 659 @I … … 672 672 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 673 673 whd in maps_assm:(??%%); 674 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1674 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 675 675 [2: normalize nodelta #absurd destruct(absurd) ] 676 676 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 677 677 whd in ⊢ (??%?); 678 678 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 679 whd in ⊢ (??%?); 680 inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta 681 @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl)) 682 [1: 683 @eq_f2 try % 684 @(pose … (set_clock ????)) #status #status_refl 685 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 686 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 687 |2: 688 @set_arg_8_status_of_pseudo_status try % 689 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 690 ] 679 change with (set_arg_8 ??? ACC_A ? = ?) 680 [2: @I ] 681 @set_arg_8_status_of_pseudo_status try % 682 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % 683 @eq_f2 try % @sym_eq 684 @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try % 685 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 691 686 |2: 692 687 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 693 688 whd in maps_assm:(??%%); 694 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1689 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 695 690 [2: normalize nodelta #absurd destruct(absurd) ] 696 691 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 697 692 whd in ⊢ (??%?); 698 693 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 699 whd in ⊢ (??%?); 700 @let_pair_in_status_of_pseudo_status 701 [1: 702 @eq_f2 try % 703 @(pose … (set_clock ????)) #status #status_refl 704 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 705 >EQs >EQticks 706 [1: 707 @sym_eq @set_clock_status_of_pseudo_status % 708 |2: 709 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 710 |3: 711 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) % 712 ] 713 |2: 714 #carry #result 715 @sym_eq @set_arg_8_status_of_pseudo_status try % 716 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 717 ] 694 change with (set_arg_8 ??? (REGISTER w) ? = ?) 695 [2: @I ] 696 @set_arg_8_status_of_pseudo_status try % 697 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) 698 [1: /2 by refl, eq_false_to_notb/ ] try % 699 @eq_f2 try % @sym_eq 700 @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try % 701 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 718 702 |3: 719 703 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 720 704 whd in maps_assm:(??%%); 721 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1705 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 722 706 [2: normalize nodelta #absurd destruct(absurd) ] 723 707 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 724 708 whd in ⊢ (??%?); 725 709 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 726 whd in ⊢ (??%?); 727 @let_pair_in_status_of_pseudo_status 728 [1: 729 @eq_f2 try % 730 @(pose … (set_clock ????)) #status #status_refl 731 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 732 >EQs >EQticks 733 [1: 734 @sym_eq @set_clock_status_of_pseudo_status % 735 |2: 736 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 737 |3: 738 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) % 739 ] 740 |2: 741 #carry #result 742 @sym_eq @set_arg_8_status_of_pseudo_status try % 743 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 744 ] 710 change with (set_arg_8 ??? (DIRECT w) ? = ?) 711 [2: /2 by refl, eq_false_to_notb/ ] 712 @set_arg_8_status_of_pseudo_status try % 713 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) 714 [1,2,3: % ] 715 @eq_f2 try % @sym_eq 716 @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try % 717 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 745 718 |4: 746 719 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 747 720 whd in maps_assm:(??%%); 748 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1721 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 749 722 [2: normalize nodelta #absurd destruct(absurd) ] 750 723 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 751 724 whd in ⊢ (??%?); 752 725 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 753 whd in ⊢ (??%?); 754 @let_pair_in_status_of_pseudo_status 755 [1: 756 @eq_f2 try % 757 @(pose … (set_clock ????)) #status #status_refl 758 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl 759 >EQs >EQticks 760 [1: 761 @sym_eq @set_clock_status_of_pseudo_status % 726 change with (set_arg_8 ??? (INDIRECT w) ? = ?) 727 [2: /2 by refl, eq_false_to_notb/ ] 728 @set_arg_8_status_of_pseudo_status try % 729 [1: 730 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 731 |2: 732 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) try % 733 @eq_f2 try % @sym_eq 734 @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try % 735 [1: 736 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % 762 737 |2: 763 738 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % 764 |3:765 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %766 ]767 |2:768 #carry #result769 @sym_eq @set_arg_8_status_of_pseudo_status try %770 [1:771 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %772 |2:773 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %774 739 ] 775 740 ] … … 783 748 [1: 784 749 @eq_f2 try % 785 @ (pose … (set_clock ????)) #status #status_refl786 @ sym_eq @(get_8051_sfr_status_of_pseudo_status … M'… status) >status_refl -status_refl750 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 751 @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl 787 752 >EQs >EQticks % 788 753 |2: 789 #carry #bl 790 @sym_eq @let_pair_in_status_of_pseudo_status 754 #carry #bl @let_pair_in_status_of_pseudo_status 791 755 [1: 792 756 @eq_f3 try % 793 @ (pose … (set_clock ????)) #status #status_refl794 @ sym_eq @(get_8051_sfr_status_of_pseudo_status … M'… status) >status_refl -status_refl757 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 758 @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl 795 759 >EQs >EQticks % 796 760 |2: 797 #carry' #bu 798 @sym_eq @set_8051_sfr_status_of_pseudo_status % 761 #carry' #bu @set_8051_sfr_status_of_pseudo_status % 799 762 ] 800 763 ] … … 806 769 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 807 770 whd in maps_assm:(??%%); 808 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1771 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 809 772 [2: normalize nodelta #absurd destruct(absurd) ] 810 773 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 815 778 [1: 816 779 @eq_f3 try % 817 @ (pose … (set_clock ????)) #status #status_refl818 @ sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl780 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 781 @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl 819 782 >EQs >EQticks try % 820 783 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 821 784 |2: 822 785 #result #flags 823 @s ym_eq @set_arg_8_status_of_pseudo_status try %786 @set_arg_8_status_of_pseudo_status try % 824 787 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 825 788 ] … … 827 790 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 828 791 whd in maps_assm:(??%%); 829 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1792 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 830 793 [2: normalize nodelta #absurd destruct(absurd) ] 831 794 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 836 799 [1: 837 800 @eq_f3 try % 838 @ (pose … (set_clock ????)) #status #status_refl839 @ sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl801 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 802 @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl 840 803 >EQs >EQticks try % 841 804 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 842 805 |2: 843 806 #result #flags 844 @s ym_eq @set_arg_8_status_of_pseudo_status try %807 @set_arg_8_status_of_pseudo_status try % 845 808 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % 846 809 ] … … 848 811 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 849 812 whd in maps_assm:(??%%); 850 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1813 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 851 814 [2: normalize nodelta #absurd destruct(absurd) ] 852 815 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 857 820 [1: 858 821 @eq_f3 try % 859 @ (pose … (set_clock ????)) #status #status_refl860 @ sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl822 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 823 @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl 861 824 >EQs >EQticks try % 862 825 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 863 826 |2: 864 827 #result #flags 865 @s ym_eq @set_arg_8_status_of_pseudo_status try %828 @set_arg_8_status_of_pseudo_status try % 866 829 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % 867 830 ] … … 869 832 #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 870 833 whd in maps_assm:(??%%); 871 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1834 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 872 835 [2: normalize nodelta #absurd destruct(absurd) ] 873 836 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 878 841 [1: 879 842 @eq_f3 try % 880 @ (pose … (set_clock ????)) #status #status_refl881 @ sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl843 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 844 @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl 882 845 >EQs >EQticks try % 883 846 [1: … … 888 851 |2: 889 852 #result #flags 890 @s ym_eq @set_arg_8_status_of_pseudo_status try %853 @set_arg_8_status_of_pseudo_status try % 891 854 [1: 892 855 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % … … 902 865 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 903 866 whd in maps_assm:(??%%); 904 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 867 inversion (assert_data ?????) in maps_assm; 868 @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1 905 869 [2: normalize nodelta #absurd destruct(absurd) ] 906 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_2870 inversion (assert_data ?????) #addressing_mode_ok_assm_2 907 871 [2: normalize nodelta #absurd destruct(absurd) ] 908 872 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 915 879 [1: 916 880 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 917 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) 918 % 881 whd in ⊢ (??%?); 882 whd in addressing_mode_ok_assm_1:(??%?); cases accA in addressing_mode_ok_assm_1; 883 normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ % 919 884 |2: 920 885 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) % 921 886 ] 922 887 ] 923 @s ym_eq @set_8051_sfr_status_of_pseudo_status888 @set_8051_sfr_status_of_pseudo_status 924 889 [2: 925 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 890 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … ACC_A … addressing_mode_ok_assm_1) 891 [2: /2 by refl, eq_false_to_notb/ ] 926 892 @eq_f @eq_f2 try % @eq_f2 @eq_f 927 893 @sym_eq 928 894 [1: 929 895 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 930 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 931 |2: 932 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) % 933 ] 934 ] 935 @sym_eq @set_clock_status_of_pseudo_status 896 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 897 cases accA in addressing_mode_ok_assm_1; 898 normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ % 899 |2: 900 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) % 901 ] 902 ] 903 @set_clock_status_of_pseudo_status 936 904 [2: 937 905 @eq_f % 938 906 ] 939 @s ym_eq @set_program_counter_status_of_pseudo_status %907 @set_program_counter_status_of_pseudo_status % 940 908 |7,8: (* DIV *) 941 909 (* XXX: work on the right hand side *) … … 944 912 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 945 913 whd in maps_assm:(??%%); 946 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 914 inversion (assert_data ?????) in maps_assm; 915 @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1 947 916 [2,4: normalize nodelta #absurd destruct(absurd) ] 948 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_2917 inversion (assert_data ?????) #addressing_mode_ok_assm_2 949 918 [2,4: normalize nodelta #absurd destruct(absurd) ] 950 919 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 952 921 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 953 922 whd in ⊢ (??%?); normalize nodelta 954 @(match_nat_status_of_pseudo_status M'cm sigma policy)923 @(match_nat_status_of_pseudo_status 〈low, high, accA〉 cm sigma policy) 955 924 [1,4: 956 925 @eq_f 957 926 @sym_eq @(pose … (set_clock ????)) #status #status_refl 958 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M'… status) >status_refl -status_refl try %927 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try % 959 928 |2,5: 960 929 @sym_eq @set_flags_status_of_pseudo_status % 961 930 |3,6: 962 931 #n @sym_eq @set_flags_status_of_pseudo_status try % 963 @s ym_eq @set_8051_sfr_status_of_pseudo_status932 @set_8051_sfr_status_of_pseudo_status 964 933 [1,3: 965 @sym_eq @set_8051_sfr_status_of_pseudo_status try % 966 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta 967 @eq_f @eq_f2 try % @eq_f 968 @(pose … (set_clock ????)) #status #status_refl 969 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 970 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 934 @set_8051_sfr_status_of_pseudo_status try % 935 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 936 cases accA in addressing_mode_ok_assm_1; normalize nodelta 937 [2,4: #address_entry #absurd destruct(absurd) ] #_ 938 @eq_f @eq_f2 % 971 939 |2,4: 972 940 whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f 973 941 @(pose … (set_clock ????)) #status #status_refl 974 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 975 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 942 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try % 943 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 944 cases accA in addressing_mode_ok_assm_1; normalize nodelta 945 [2,4: #address_entry #absurd destruct(absurd) ] #_ % 976 946 ] 977 947 ] … … 982 952 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 983 953 whd in maps_assm:(??%%); 984 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 954 inversion (assert_data ?????) in maps_assm; 955 @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1 985 956 [2: normalize nodelta #absurd destruct(absurd) ] 986 957 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 992 963 @eq_f normalize nodelta >EQs >EQticks <instr_refl 993 964 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 994 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 965 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 966 cases accA in addressing_mode_ok_assm_1; normalize nodelta 967 [2: #address_entry #absurd destruct(absurd) ] #_ % 995 968 |2: 996 969 @(pair_replace ?????????? p) … … 1005 978 |2: 1006 979 change with (get_ac_flag ??? = get_ac_flag ???) 1007 @(get_ac_flag_status_of_pseudo_status M')1008 @s ym_eq @set_clock_status_of_pseudo_status980 @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉) 981 @set_clock_status_of_pseudo_status 1009 982 >EQs >EQticks <instr_refl % 1010 983 ] … … 1014 987 [1: 1015 988 @eq_f3 try % normalize nodelta 1016 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) 1017 whd in ⊢ (??%?); 1018 >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 989 @(get_8051_sfr_status_of_pseudo_status 〈low, high, accA〉 … policy … (refl …)) 990 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 991 cases accA in addressing_mode_ok_assm_1; normalize nodelta 992 [2: #address_entry #absurd destruct(absurd) ] #_ 993 >EQs >EQticks <instr_refl % 1019 994 |2: 1020 995 @(pair_replace ?????????? p2) try % … … 1023 998 @(if_then_else_replace ???????? p4) try % normalize nodelta 1024 999 @(if_then_else_replace ???????? p4) try % normalize nodelta 1025 @(pair_replace ?????????? p5) try %1026 @(pair_replace ?????????? p5) try %1027 1000 @set_flags_status_of_pseudo_status try % 1028 1001 [1: 1029 @eq_f @(get_ac_flag_status_of_pseudo_status M')1030 @s ym_eq @set_8051_sfr_status_of_pseudo_status1002 @eq_f @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉) 1003 @set_8051_sfr_status_of_pseudo_status 1031 1004 [1: 1032 @s ym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %1005 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1033 1006 |2: 1034 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1007 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1008 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1009 [2: #address_entry #absurd destruct(absurd) ] #_ % 1035 1010 ] 1036 1011 |2: 1037 @(get_ov_flag_status_of_pseudo_status M')1038 @s ym_eq @set_8051_sfr_status_of_pseudo_status1012 @(get_ov_flag_status_of_pseudo_status 〈low, high, accA〉) 1013 @set_8051_sfr_status_of_pseudo_status 1039 1014 [1: 1040 @s ym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %1015 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1041 1016 |2: 1042 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1017 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1018 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1019 [2: #address_entry #absurd destruct(absurd) ] #_ % 1043 1020 ] 1044 1021 |3: 1045 @s ym_eq @set_8051_sfr_status_of_pseudo_status1022 @set_8051_sfr_status_of_pseudo_status 1046 1023 [1: 1047 @s ym_eq @set_clock_status_of_pseudo_status1024 @set_clock_status_of_pseudo_status 1048 1025 [1: 1049 >EQs 1050 @sym_eq @set_program_counter_status_of_pseudo_status % 1026 >EQs @set_program_counter_status_of_pseudo_status % 1051 1027 |2: 1052 1028 >EQs >EQticks <instr_refl % 1053 1029 ] 1054 1030 |2: 1055 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1031 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1032 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1033 [2: #address_entry #absurd destruct(absurd) ] #_ % 1056 1034 ] 1057 1035 ] … … 1066 1044 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1067 1045 whd in maps_assm:(??%%); 1068 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1046 inversion (assert_data ?????) in maps_assm; 1047 @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1 1069 1048 [2: normalize nodelta #absurd destruct(absurd) ] 1070 1049 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1076 1055 @eq_f normalize nodelta >EQs >EQticks <instr_refl 1077 1056 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1078 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1057 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1058 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1059 [2: #address_entry #absurd destruct(absurd) ] #_ % 1079 1060 |2: 1080 1061 @(pair_replace ?????????? p) … … 1089 1070 |2: 1090 1071 change with (get_ac_flag ??? = get_ac_flag ???) 1091 @(get_ac_flag_status_of_pseudo_status M')1092 @s ym_eq @set_clock_status_of_pseudo_status1072 @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉) 1073 @set_clock_status_of_pseudo_status 1093 1074 >EQs >EQticks <instr_refl % 1094 1075 ] … … 1098 1079 [1: 1099 1080 @eq_f3 try % normalize nodelta 1100 @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) 1101 whd in ⊢ (??%?); 1102 >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1081 @(get_8051_sfr_status_of_pseudo_status 〈low, high, accA〉 … policy … (refl …)) 1082 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1083 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1084 [2: #address_entry #absurd destruct(absurd) ] #_ >EQs >EQticks <instr_refl % 1103 1085 |2: 1104 1086 @(pair_replace ?????????? p2) try % … … 1109 1091 @set_clock_status_of_pseudo_status 1110 1092 [1: 1111 >EQs 1112 @sym_eq @set_program_counter_status_of_pseudo_status % 1093 >EQs @set_program_counter_status_of_pseudo_status % 1113 1094 |2: 1114 1095 >EQs >EQticks <instr_refl % … … 1124 1105 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1125 1106 whd in maps_assm:(??%%); 1126 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1107 inversion (assert_data ?????) in maps_assm; 1108 @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1 1127 1109 [2: normalize nodelta #absurd destruct(absurd) ] 1128 1110 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1134 1116 @eq_f normalize nodelta >EQs >EQticks <instr_refl 1135 1117 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1136 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1118 whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?); 1119 cases accA in addressing_mode_ok_assm_1; normalize nodelta 1120 [2: #address_entry #absurd destruct(absurd) ] #_ % 1137 1121 |2: 1138 1122 @(pair_replace ?????????? p) … … 1147 1131 |2: 1148 1132 change with (get_ac_flag ??? = get_ac_flag ???) 1149 @(get_ac_flag_status_of_pseudo_status M')1150 @s ym_eq @set_clock_status_of_pseudo_status1133 @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉) 1134 @set_clock_status_of_pseudo_status 1151 1135 >EQs >EQticks <instr_refl % 1152 1136 ] … … 1155 1139 @set_clock_status_of_pseudo_status 1156 1140 [1: 1157 >EQs 1158 @sym_eq @set_program_counter_status_of_pseudo_status % 1141 >EQs @set_program_counter_status_of_pseudo_status % 1159 1142 |2: 1160 1143 >EQs >EQticks <instr_refl % … … 1580 1563 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1581 1564 inversion sj_possible #sj_possible_refl normalize nodelta 1565 @(subaddressing_mode_elim … addr1) #w 1582 1566 [1: 1583 1567 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1590 1574 >EQs >EQticks <instr_refl normalize nodelta 1591 1575 [1: 1592 @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try % 1593 @(subaddressing_mode_elim … addr1) #w whd 1576 @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try % whd 1577 @vsplit_elim #bit_1 #seven_bits #bit_1_seven_bits_refl normalize nodelta 1578 inversion (head' bool ??) #head_refl' normalize nodelta 1579 @vsplit_elim #four_bits #three_bits #four_bits_three_bits_refl normalize nodelta 1580 whd in ⊢ (??%%); cases (sfr_of_Byte ?) normalize nodelta 1594 1581 |2: 1595 1582 @set_program_counter_status_of_pseudo_status … … 1637 1624 @(if_then_else_replace ???????? p) normalize nodelta 1638 1625 [1: 1626 @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉 … (BIT_ADDR w)) 1627 1639 1628 @eq_f >EQs 1640 1629 whd in match get_cy_flag; normalize nodelta … … 1675 1664 ] 1676 1665 ] 1677 | 16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)1666 |*)16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) 1678 1667 cases daemon 1679 1668 |(*29,30: (* ANL and ORL *) … … 1686 1675 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1687 1676 whd in maps_assm:(??%%); 1688 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11677 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1689 1678 [2,4: normalize nodelta #absurd destruct(absurd) ] 1690 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_21679 inversion (assert_data ?????) #addressing_mode_ok_assm_2 1691 1680 [2,4: normalize nodelta #absurd destruct(absurd) ] 1692 1681 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1736 1725 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1737 1726 whd in maps_assm:(??%%); 1738 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11727 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1739 1728 [2,4: normalize nodelta #absurd destruct(absurd) ] 1740 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_21729 inversion (assert_data ?????) #addressing_mode_ok_assm_2 1741 1730 [2,4: normalize nodelta #absurd destruct(absurd) ] 1742 1731 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1787 1776 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1788 1777 whd in maps_assm:(??%%); 1789 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11778 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1790 1779 [2,4: normalize nodelta #absurd destruct(absurd) ] 1791 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_21780 inversion (assert_data ?????) #addressing_mode_ok_assm_2 1792 1781 [2,4: normalize nodelta #absurd destruct(absurd) ] 1793 1782 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1806 1795 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1807 1796 whd in maps_assm:(??%%); 1808 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11797 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1809 1798 [2: normalize nodelta #absurd destruct(absurd) ] 1810 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_21799 inversion (assert_data ?????) #addressing_mode_ok_assm_2 1811 1800 [2: normalize nodelta #absurd destruct(absurd) ] 1812 1801 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1855 1844 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1856 1845 whd in maps_assm:(??%%); 1857 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11846 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1858 1847 [2: normalize nodelta #absurd destruct(absurd) ] 1859 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_21848 inversion (assert_data ?????) #addressing_mode_ok_assm_2 1860 1849 [2: normalize nodelta #absurd destruct(absurd) ] 1861 1850 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1907 1896 whd in maps_assm:(??%%); 1908 1897 [1,2: 1909 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11898 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1910 1899 [2,4: normalize nodelta #absurd destruct(absurd) ] 1911 1900 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1941 1930 whd in maps_assm:(??%%); 1942 1931 [1,2: 1943 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_11932 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 1944 1933 [2,4: normalize nodelta #absurd destruct(absurd) ] 1945 1934 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 1989 1978 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1990 1979 whd in maps_assm:(??%%); 1991 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm1980 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm 1992 1981 [2,4: normalize nodelta #absurd destruct(absurd) ] 1993 1982 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2012 2001 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2013 2002 whd in maps_assm:(??%%); 2014 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm2003 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm 2015 2004 [2,4: normalize nodelta #absurd destruct(absurd) ] 2016 2005 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2038 2027 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2039 2028 whd in maps_assm:(??%%); 2040 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12029 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2041 2030 [2: normalize nodelta #absurd destruct(absurd) ] 2042 2031 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2093 2082 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2094 2083 whd in maps_assm:(??%%); 2095 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12084 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2096 2085 [2: normalize nodelta #absurd destruct(absurd) ] 2097 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22086 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2098 2087 [2: normalize nodelta #absurd destruct(absurd) ] 2099 2088 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2132 2121 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2133 2122 whd in maps_assm:(??%%); 2134 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12123 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2135 2124 [2: normalize nodelta #absurd destruct(absurd) ] 2136 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22125 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2137 2126 [2: normalize nodelta #absurd destruct(absurd) ] 2138 2127 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2171 2160 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2172 2161 whd in maps_assm:(??%%); 2173 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12162 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2174 2163 [2: normalize nodelta #absurd destruct(absurd) ] 2175 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22164 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2176 2165 [2: normalize nodelta #absurd destruct(absurd) ] 2177 2166 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2210 2199 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2211 2200 whd in maps_assm:(??%%); 2212 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12201 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2213 2202 [2: normalize nodelta #absurd destruct(absurd) ] 2214 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22203 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2215 2204 [2: normalize nodelta #absurd destruct(absurd) ] 2216 2205 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2227 2216 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2228 2217 whd in maps_assm:(??%%); 2229 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12218 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2230 2219 [2: normalize nodelta #absurd destruct(absurd) ] 2231 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22220 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2232 2221 [2: normalize nodelta #absurd destruct(absurd) ] 2233 2222 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2250 2239 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2251 2240 whd in maps_assm:(??%%); 2252 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12241 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2253 2242 [2: normalize nodelta #absurd destruct(absurd) ] 2254 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22243 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2255 2244 [2: normalize nodelta #absurd destruct(absurd) ] 2256 2245 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2286 2275 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2287 2276 whd in maps_assm:(??%%); 2288 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12277 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2289 2278 [2: normalize nodelta #absurd destruct(absurd) ] 2290 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22279 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2291 2280 [2: normalize nodelta #absurd destruct(absurd) ] 2292 2281 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2319 2308 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2320 2309 whd in maps_assm:(??%%); 2321 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12310 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2322 2311 [2: normalize nodelta #absurd destruct(absurd) ] 2323 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22312 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2324 2313 [2: normalize nodelta #absurd destruct(absurd) ] 2325 2314 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2356 2345 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2357 2346 whd in maps_assm:(??%%); 2358 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12347 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2359 2348 [2: normalize nodelta #absurd destruct(absurd) ] 2360 2349 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2436 2425 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2437 2426 whd in maps_assm:(??%%); 2438 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12427 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2439 2428 [2: normalize nodelta #absurd destruct(absurd) ] 2440 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22429 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2441 2430 [2: normalize nodelta #absurd destruct(absurd) ] 2442 2431 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) … … 2487 2476 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2488 2477 whd in maps_assm:(??%%); 2489 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_12478 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 2490 2479 [2: normalize nodelta #absurd destruct(absurd) ] 2491 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_22480 inversion (assert_data ?????) #addressing_mode_ok_assm_2 2492 2481 [2: normalize nodelta #absurd destruct(absurd) ] 2493 2482 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
Note: See TracChangeset
for help on using the changeset viewer.
