Changeset 2181 for src/ASM/Test.ma
- Timestamp:
- Jul 13, 2012, 11:00:04 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2173 r2181 19 19 status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. 20 20 #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // 21 qed. 22 23 lemma if_then_else_status_of_pseudo_status_true: 24 ∀M: internal_pseudo_address_map. 25 ∀cm: pseudo_assembly_program. 26 ∀sigma: Word → Word. 27 ∀policy: Word → bool. 28 ∀s, s', s'', s'''. 29 ∀t: bool. 30 t = true → 31 status_of_pseudo_status M cm s sigma policy = s' → 32 if t then 33 s' 34 else 35 s'' = 36 status_of_pseudo_status M cm (if t then s else s''') sigma policy. 37 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl 38 >t_refl normalize nodelta >s_refl % 39 qed. 40 41 lemma if_then_else_status_of_pseudo_status_false: 42 ∀M: internal_pseudo_address_map. 43 ∀cm: pseudo_assembly_program. 44 ∀sigma: Word → Word. 45 ∀policy: Word → bool. 46 ∀s, s', s'', s'''. 47 ∀t: bool. 48 t = false → 49 status_of_pseudo_status M cm s sigma policy = s' → 50 if t then 51 s'' 52 else 53 s' = 54 status_of_pseudo_status M cm (if t then s''' else s) sigma policy. 55 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl 56 >t_refl normalize nodelta >s_refl % 21 57 qed. 22 58 … … 225 261 226 262 lemma get_index_v_status_of_pseudo_status: 227 ∀M, code_memory, sigma, policy, s, sfr. 228 (get_index_v Byte 19 263 ∀M, code_memory, sigma, policy, s, s', sfr. 264 map_address_using_internal_pseudo_address_map M sigma sfr 265 (get_index_v Byte 19 266 (special_function_registers_8051 pseudo_assembly_program code_memory s) 267 (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' → 268 get_index_v Byte 19 229 269 (special_function_registers_8051 (BitVectorTrie Byte 16) 230 270 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 231 271 (status_of_pseudo_status M code_memory s sigma policy)) 232 (sfr_8051_index sfr) (sfr8051_index_19 sfr) = 233 map_address_using_internal_pseudo_address_map M sigma sfr 234 (get_index_v Byte 19 235 (special_function_registers_8051 pseudo_assembly_program code_memory s) 236 (sfr_8051_index sfr) (sfr8051_index_19 sfr))). 237 #M #code_memory #sigma #policy #s #sfr 272 (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'. 273 #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl 238 274 whd in match status_of_pseudo_status; normalize nodelta 239 275 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta … … 275 311 276 312 lemma get_8051_sfr_status_of_pseudo_status: 277 ∀M, code_memory, sigma, policy, s, s', s fr.313 ∀M, code_memory, sigma, policy, s, s', s'', sfr. 278 314 status_of_pseudo_status M code_memory s sigma policy = s' → 279 (get_8051_sfr (BitVectorTrie Byte 16) 315 map_address_using_internal_pseudo_address_map M sigma sfr 316 (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' → 317 get_8051_sfr (BitVectorTrie Byte 16) 280 318 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 281 s' sfr = 282 map_address_using_internal_pseudo_address_map M sigma sfr 283 (get_8051_sfr pseudo_assembly_program code_memory s sfr)). 284 #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl 319 s' sfr = s''. 320 #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl' 285 321 whd in match get_8051_sfr; normalize nodelta 286 @get_index_v_status_of_pseudo_status 322 @get_index_v_status_of_pseudo_status % 287 323 qed. 288 324 … … 444 480 bit_address_of_register … cm s r. 445 481 #M #cm #s #sigma #policy #r whd in ⊢ (??%%); 446 >(get_8051_sfr_status_of_pseudo_status … (refl …) )482 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 447 483 @pair_elim #un #ln #_ 448 484 @pair_elim #r1 #r0 #_ % … … 452 488 primitive *) 453 489 axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: 454 ∀M,sigma,cm,s,addr. 490 ∀M,sigma,cm,s,s',addr. 491 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) 492 (lookup Byte 7 addr 493 (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 455 494 lookup Byte 7 addr 456 495 (low_internal_ram_of_pseudo_low_internal_ram M 457 496 (low_internal_ram pseudo_assembly_program cm s)) (zero 8) 458 = 459 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) 460 (lookup Byte 7 addr 461 (low_internal_ram pseudo_assembly_program cm s) (zero 8)). 497 = s'. 462 498 463 499 (*CSC: provable using the axiom in AssemblyProof, but this one seems more 464 500 primitive *) 465 501 axiom lookup_high_internal_ram_of_pseudo_high_internal_ram: 466 ∀M,sigma,cm,s,addr. 502 ∀M,sigma,cm,s,s',addr. 503 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) 504 (lookup Byte 7 addr 505 (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 467 506 lookup Byte 7 addr 468 507 (high_internal_ram_of_pseudo_high_internal_ram M 469 508 (high_internal_ram pseudo_assembly_program cm s)) (zero 8) 470 = 471 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) 472 (lookup Byte 7 addr 473 (high_internal_ram pseudo_assembly_program cm s) (zero 8)). 509 = s'. 474 510 475 511 lemma get_register_status_of_pseudo_status: 476 ∀M,cm,sigma,policy,s,s', r.512 ∀M,cm,sigma,policy,s,s',s'',r. 477 513 status_of_pseudo_status M cm s sigma policy = s' → 514 map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) 515 (get_register … cm s r) = s'' → 478 516 get_register … 479 517 (code_memory_of_pseudo_assembly_program cm sigma policy) 480 s' r = 481 map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) 482 (get_register … cm s r). 483 #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta 518 s' r = s''. 519 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl' 520 whd in match get_register; normalize nodelta 484 521 whd in match status_of_pseudo_status; normalize nodelta 485 522 >bit_address_of_register_status_of_pseudo_status 486 @ lookup_low_internal_ram_of_pseudo_low_internal_ram523 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …)) 487 524 qed. 488 525 … … 586 623 qed. 587 624 588 lemma set_arg_8_status_of_pseudo_status :625 lemma set_arg_8_status_of_pseudo_status': 589 626 ∀cm. 590 627 ∀ps. … … 654 691 | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 655 692 |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; 656 >(get_register_status_of_pseudo_status … (refl …) )693 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 657 694 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 658 695 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta … … 660 697 | >(insert_low_internal_ram_status_of_pseudo_status … v) ] 661 698 // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 662 |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) )699 |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 663 700 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 664 701 >EQ1 normalize nodelta … … 667 704 |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/ 668 705 |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status % 669 |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) )670 >(get_8051_sfr_status_of_pseudo_status … (refl …) )706 |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 707 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 671 708 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] % 709 qed. 710 711 lemma set_arg_8_status_of_pseudo_status: 712 ∀cm. 713 ∀ps. 714 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 715 ∀value. 716 ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. 717 status_of_pseudo_status M cm ps sigma policy = s' → 718 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 719 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → 720 set_arg_8 (BitVectorTrie Byte 16) 721 (code_memory_of_pseudo_assembly_program cm sigma policy) 722 s' addr value' = 723 status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. 724 #cm #ps #addr #value 725 cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant 726 @relevant 672 727 qed. 673 728 … … 754 809 ∀d: Byte. 755 810 ∀l: bool. 756 ∀M. ∀sigma. ∀policy. ∀s'. 811 ∀M. ∀sigma. ∀policy. ∀s'. ∀s''. 812 map_address_Byte_using_internal_pseudo_address_map M sigma 813 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' → 757 814 (status_of_pseudo_status M code_memory s sigma policy) = s' → 758 815 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 759 816 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 760 s' d l = 761 map_address_Byte_using_internal_pseudo_address_map M sigma 762 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). 763 #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ 764 #H @H 817 s' d l) = s''. 818 #code #s #d #v 819 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant 820 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant % 765 821 qed. 766 822 767 823 lemma program_counter_status_of_pseudo_status: 768 ∀M. ∀sigma . ∀policy.824 ∀M. ∀sigma: Word → Word. ∀policy. 769 825 ∀code_memory: pseudo_assembly_program. 770 826 ∀s: PreStatus ? code_memory. 771 827 ∀s'. 828 ∀s''. 829 sigma (program_counter … s) = s'' → 772 830 (status_of_pseudo_status M code_memory s sigma policy) = s' → 773 831 program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) 774 s' = 775 sigma (program_counter … s). 776 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl // 832 s' = s''. 833 #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' // 777 834 qed. 778 835 … … 786 843 #M #cm #sigma #policy #s #s' #s_refl <s_refl 787 844 whd in match get_cy_flag; normalize nodelta 788 > get_index_v_status_of_pseudo_status%789 qed. 790 791 lemma get_arg_8_status_of_pseudo_status :845 >(get_index_v_status_of_pseudo_status … (refl …)) % 846 qed. 847 848 lemma get_arg_8_status_of_pseudo_status': 792 849 ∀cm. 793 850 ∀ps. … … 850 907 [1: 851 908 #_ >p normalize nodelta >p1 normalize nodelta 852 @ get_bit_addressable_sfr_status_of_pseudo_status%909 @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) % 853 910 |2: 854 911 #_>p normalize nodelta >p1 normalize nodelta 855 @ lookup_low_internal_ram_of_pseudo_low_internal_ram912 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) % 856 913 |3,4: 857 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) )914 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 858 915 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 859 916 >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta 860 917 [1: 861 >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)918 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma) 862 919 |2: 863 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)920 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) 864 921 ] 865 922 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 866 923 |5: 867 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) )924 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 868 925 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 869 926 >assoc_list_assm normalize nodelta % 870 927 |6,7,8,9: 871 #_ /2 /928 #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/ 872 929 |10: 873 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) )874 >(get_8051_sfr_status_of_pseudo_status … (refl …) )875 >(get_8051_sfr_status_of_pseudo_status … (refl …) )930 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 931 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 932 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 876 933 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 877 934 >acc_a_assm >p normalize nodelta // 878 935 |11: 879 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) )880 >(program_counter_status_of_pseudo_status … (refl …) )936 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 937 >(program_counter_status_of_pseudo_status … (refl …) (refl …)) 881 938 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 882 939 >sigma_assm >map_acc_a_assm >p normalize nodelta // 883 940 |12: 884 #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) )885 >(get_8051_sfr_status_of_pseudo_status … (refl …) )941 #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 942 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 886 943 >external_ram_status_of_pseudo_status // 887 944 ] 945 qed. 946 947 lemma get_arg_8_status_of_pseudo_status: 948 ∀cm. 949 ∀ps. 950 ∀l. 951 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 952 ∀M. ∀sigma. ∀policy. ∀s', s''. 953 (status_of_pseudo_status M cm ps sigma policy) = s' → 954 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' → 955 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 956 get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 957 s' l addr = s''. 958 #cm #ps #l #addr 959 cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant 960 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl' 961 @relevant assumption 888 962 qed. 889 963 … … 1017 1091 |2,4: 1018 1092 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1019 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) ) #map_address_assm1093 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm 1020 1094 >map_address_assm % 1021 1095 |3,5: 1022 1096 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1023 1097 whd in match status_of_pseudo_status; normalize nodelta 1024 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma )1098 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1025 1099 #map_address_assm >map_address_assm % 1026 1100 ] … … 1106 1180 qed. 1107 1181 1108 lemma set_arg_1_status_of_pseudo_status :1182 lemma set_arg_1_status_of_pseudo_status': 1109 1183 ∀cm: pseudo_assembly_program. 1110 1184 ∀ps: PreStatus pseudo_assembly_program cm. 1111 1185 ∀addr: [[bit_addr; carry]]. 1112 1186 ∀b: Bit. 1113 Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. 1187 Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'. 1188 b = b' → 1114 1189 status_of_pseudo_status M cm ps sigma policy = s' → 1115 1190 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → … … 1118 1193 (code_memory_of_pseudo_assembly_program cm sigma policy) 1119 1194 s' addr b = 1120 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b ) sigma policy.1195 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy. 1121 1196 whd in match set_arg_1; normalize nodelta 1122 1197 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta … … 1157 1232 [ ] 1158 1233 ] (subaddressing_modein … a)) normalize nodelta 1159 try @modulus_less_than #M #sigma #policy #s' # s_refl <s_refl1234 try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl 1160 1235 [1: 1161 #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) )1236 #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 1162 1237 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1163 1238 >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % 1164 1239 |2,3: 1165 >(get_8051_sfr_status_of_pseudo_status … (refl …) )1240 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 1166 1241 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1167 1242 >p normalize nodelta >p1 normalize nodelta 1168 1243 #map_bit_address_assm_1 #map_bit_address_assm_2 1169 1244 [1: 1170 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) )1245 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) 1171 1246 >map_bit_address_assm_1 1172 1247 >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) % 1173 1248 |2: 1174 1249 whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta 1175 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma )1250 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1176 1251 >map_bit_address_assm_1 1177 1252 >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2) … … 1179 1254 ] 1180 1255 ] 1256 qed. 1257 1258 lemma set_arg_1_status_of_pseudo_status: 1259 ∀cm: pseudo_assembly_program. 1260 ∀ps: PreStatus pseudo_assembly_program cm. 1261 ∀addr: [[bit_addr; carry]]. 1262 ∀b: Bit. 1263 ∀M. ∀sigma. ∀policy. ∀s'. ∀b'. 1264 b = b' → 1265 status_of_pseudo_status M cm ps sigma policy = s' → 1266 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → 1267 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b → 1268 set_arg_1 (BitVectorTrie Byte 16) 1269 (code_memory_of_pseudo_assembly_program cm sigma policy) 1270 s' addr b = 1271 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy. 1272 #cm #ps #addr #b 1273 cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant 1274 @relevant 1181 1275 qed. 1182 1276 … … 1201 1295 #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl // 1202 1296 qed. 1297 1298 lemma let_pair_in_status_of_pseudo_status: 1299 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1300 c = c' → 1301 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') → 1302 let 〈left, right〉 ≝ c' in s' left right c' = 1303 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. 1304 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta // 1305 qed. 1306 1307 lemma let_pair_as_in_status_of_pseudo_status: 1308 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1309 ∀c_refl: c = c'. 1310 (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) → 1311 let 〈left, right〉 as H ≝ c' in s' left right H c = 1312 status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy. 1313 [2: >H' assumption ] 1314 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' 1315 #destruct_assm destruct(destruct_assm) normalize nodelta 1316 #status_of_pseudo_status_assm >status_of_pseudo_status_assm // 1317 qed. 1318 1319 lemma if_then_else_status_of_pseudo_status: 1320 ∀M: internal_pseudo_address_map. 1321 ∀cm: pseudo_assembly_program. 1322 ∀sigma: Word → Word. 1323 ∀policy: Word → bool. 1324 ∀s, s', s'', s'''. 1325 ∀t, t': bool. 1326 t = t' → 1327 status_of_pseudo_status M cm s sigma policy = s' → 1328 status_of_pseudo_status M cm s'' sigma policy = s''' → 1329 if t then 1330 s' 1331 else 1332 s''' = 1333 status_of_pseudo_status M cm (if t' then s else s'') sigma policy. 1334 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl 1335 >t_refl normalize nodelta >s_refl cases t' normalize nodelta // 1336 qed.
Note: See TracChangeset
for help on using the changeset viewer.