 Timestamp:
 Jun 14, 2012, 2:18:53 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2055 r2070 461 461 qed. 462 462 463 (*definition rel_jump_length_ok ≝464 λlookup_address:Word.465 λpc:Word.466 Σjump_len:jump_length.467 (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)468 ∀(*x,*)y. expand_relative_jump_internal_safe lookup_address jump_len (*x*) pc y ≠ None ?.469 470 lemma eject_rel_jump_length: ∀x,y. rel_jump_length_ok x y → jump_length.471 #x #y #p @(pi1 … p)472 qed.473 474 coercion eject_rel_jump_length nocomposites:475 ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝476 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*)477 478 (*definition expand_relative_jump_internal:479 ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) →480 list instruction481 ≝ λlookup_address,pc,i.482 match expand_relative_jump_internal_safe lookup_address pc i483 return λres. res ≠ None ? → ?484 with485 [ None ⇒ λabs.⊥486  Some res ⇒ λ_.res ] (pi2 … jump_len i).487 cases abs /2/488 qed.*)489 490 463 definition expand_relative_jump: 491 464 ∀lookup_labels.∀sigma. … … 586 559 % 587 560 qed. 588 589 (*590 (*X?591 definition jump_length_ok ≝592 λlookup_labels:Identifier → Word.593 λpc:Word.594 Σjump_len:jump_length.595 (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)596 ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.597 *)598 599 lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.600 #x #y #p @(pi1 … p)601 qed.602 603 coercion eject_jump_length nocomposites:604 ∀x,y.∀pol:jump_length_ok x y. jump_length ≝605 eject_jump_length on _pol:(jump_length_ok ??) to jump_length.606 607 definition expand_pseudo_instruction:608 ∀lookup_labels:Identifier → Word. ∀pc:Word. jump_length_ok lookup_labels pc →609 ? → pseudo_instruction → list instruction ≝610 λlookup_labels,pc,jump_len,lookup_datalabels,i.611 match expand_pseudo_instruction_safe lookup_labels pc jump_len lookup_datalabels i612 return λres. res ≠ None ? → ?613 with614 [ None ⇒ λabs.⊥615  Some res ⇒ λ_.res ] (pi2 … jump_len lookup_datalabels i).616 cases abs /2/617 qed.618 *)619 (*X?620 definition policy_type ≝621 λlookup_labels:Identifier → Word.622 ∀pc:Word. jump_length_ok lookup_labels pc.623 *)624 625 (*definition policy_type2 ≝626 λprogram.627 Σpol:Word → jump_length.628 let lookup_labels ≝629 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in630 ∀pc:Word. let jump_len ≝ pol pc in631 ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*)632 561 633 562 definition assembly_1_pseudoinstruction ≝ … … 652 581 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 653 582 654 (* Jaap: never used655 lemma fetch_pseudo_instruction_prefix:656 ∀prefix.∀x.∀ppc.ppc < (prefix) →657 fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =658 fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).659 #prefix #x #ppc elim prefix660 [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n661  #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);662 whd in match (fetch_pseudo_instruction ((h::t)@x) ?);663 >nth_append_first664 [ //665  >nat_of_bitvector_bitvector_of_nat666 [ @Hppc667  cases daemon (* XXX invariant *)668 ]669 ]670 ]671 qed.672 *)673 674 583 (*CSC: move elsewhere *) 675 584 lemma nth_safe_append: … … 694 603 #EQ %{lbl0} @EQ 695 604 qed. 696 697 (*lemma sigma00_append:698 ∀jump_expansion,l1,l2.699 ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).700 sigma00 jump_expansion (l1@l2) acc =701 sigma00 jump_expansion702 l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)703 704 (* lemma sigma00_strict:705 ∀jump_expansion,l,acc. acc = None ? →706 sigma00 jump_expansion l acc = None ….707 #jump_expansion #l elim l708 [ #acc #H >H %709  #hd #tl #IH #acc #H >H change with (sigma00 ? tl ? = ?) @IH % ]710 qed.711 712 lemma policy_ok_prefix_ok:713 ∀program.∀pol:policy program.∀suffix,prefix.714 prefix@suffix = \snd program →715 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….716 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);717 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol718 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;719 normalize nodelta >sigma00_append720 cases (sigma00 ?? prefix ?)721 [2: #x #_ % #abs destruct(abs)722  * #abs @⊥ @abs >sigma00_strict % ]723 qed.724 725 lemma policy_ok_prefix_hd_ok:726 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.727 (prefix@[hd])@suffix = \snd program →728 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →729 let 〈ppc,pc_map〉 ≝ ppc_pc_map in730 let 〈program_counter, sigma_map〉 ≝ pc_map in731 let 〈label, i〉 ≝ hd in732 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….733 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2734 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix735 (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);736 @pair_elim #ppc #pc_map #EQ3 normalize nodelta737 @pair_elim #pc #map #EQ4 normalize nodelta738 @pair_elim #l' #i' #EQ5 normalize nodelta739 cases (construct_costs_safe ??????) normalize740 [* #abs @⊥ @abs %  #X #_ % #abs destruct(abs)]741 qed. *)742 743 (* JPB,CSC: this definition is now replaced by the expand_pseudo_instruction higher up744 definition expand_pseudo_instruction:745 ∀program:pseudo_assembly_program.∀pol: policy program.746 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.747 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →748 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →749 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in750 pc = sigma program pol ppc →751 Σres:list instruction. Some … res = expand_pseudo_instruction_safe pc (lookup_labels pi) lookup_datalabels (pol ppc) pi752 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.753 match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with754 [ None ⇒ let dummy ≝ [ ] in dummy755  Some res ⇒ res ].756 [ @⊥ whd in p:(??%??);757 generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);758 whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ?  _ ⇒ ?])?) → ?);759 generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));760 cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]761 #res #K762 cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1763 generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;764 cases daemon (* CSC: XXXXXXXX Ero qui765 766 [3: @policy_ok_prefix_ok ]767  sigma00 program pol pre768 769 770 771 QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che772 fetch ppc = hd sse program = pre @ [hd] @ tl e pre = ppc773 per concludere construct_costs_safe ≠ None *)774  >p %]775 qed. *)776 777 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *)778 (* definition assembly_1_pseudoinstruction':779 ∀program:pseudo_assembly_program.∀pol: policy program.780 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.781 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →782 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →783 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →784 Σres:(nat × (list Byte)).785 res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧786 let 〈len,code〉 ≝ res in787 sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =788 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)789 ≝ λprogram: pseudo_assembly_program.790 λpol: policy program.791 λppc: Word.792 λlookup_labels.793 λlookup_datalabels.794 λpi.795 λprf1,prf2,prf3.796 assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.797 [ @⊥ elim pi in p; [*]798 try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs799 generalize in match (jmeq_to_eq ??? abs); abs; #abs whd in abs:(??%?); try destruct(abs)800 whd in abs:(??match % with [_ ⇒ ?  _ ⇒ ?]?);801 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)802 cases daemon803  % [ >p %]804 cases res in p ⊢ %; res; #len #code #EQ normalize nodelta;805 (* THIS SHOULD BE TRUE INSTEAD *)806 cases daemon]807 qed.808 809 definition assembly_1_pseudoinstruction:810 ∀program:pseudo_assembly_program.∀pol: policy program.811 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.812 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →813 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →814 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →815 nat × (list Byte)816 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.817 assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1818 prf2 prf3.819 820 lemma assembly_1_pseudoinstruction_ok1:821 ∀program:pseudo_assembly_program.∀pol: policy program.822 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.823 ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).824 ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).825 ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.826 Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)827 = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.828 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3829 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))830 #H1 #_ @H1831 qed. *)832 833 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *)834 (* definition construct_costs':835 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.836 Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i837 ≝838 λprogram.λpol: policy program.λppc,pc,costs,i.839 match construct_costs_safe program pol ppc pc costs i with840 [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy841  Some res ⇒ res ].842 [ cases daemon843  >p %]844 qed.845 846 definition construct_costs ≝847 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i). *)848 849 (*850 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.851 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.852 853 axiom foldl_strong_step:854 ∀A:Type[0].855 ∀P: list A → Type[0].856 ∀l: list A.857 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).858 ∀acc: P [ ].859 ∀Q: ∀prefix. P prefix → Prop.860 ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.861 ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).862 Q [ ] acc →863 Q l (foldl_strong A P l H acc).864 (*865 #A #P #l #H #acc #Q #HQ #Hacc normalize;866 generalize in match867 (foldl_strong ?868 (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))869 l ? Hacc)870 [3: >suffix_of_ok %  2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]871 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)872 #K873 874 generalize in match875 (foldl_strong ?876 (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))877 [2: @H878 *)879 880 axiom foldl_elim:881 ∀A:Type[0].882 ∀B: Type[0].883 ∀H: A → B → A.884 ∀acc: A.885 ∀l: list B.886 ∀Q: A → Prop.887 (∀acc:A.∀b:B. Q acc → Q (H acc b)) →888 Q acc →889 Q (foldl A B H acc l).890 *)891 892 (*893 lemma tech_pc_sigma00_append_Some:894 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.895 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →896 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.897 #program #pol #prefix #costs #label #i #ppc #pc #H898 whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;899 whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;900 generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)901 whd in match sigma0; normalize nodelta;902 >foldl_step903 change with (? → match match sigma00 program pol prefix with [None ⇒ ?  Some res ⇒ ?] with [ None ⇒ ?  Some res ⇒ ? ] = ?)904 whd in match tech_pc_sigma00 in H; normalize nodelta in H;905 cases (sigma00 program pol prefix) in H ⊢ %906 [ whd in ⊢ (??%% → ?) #abs destruct(abs)907  * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)908 909 normalize nodelta; H;910 911 912 generalize in match H; H;913 generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ?  _ ⇒ ?] with [_ ⇒ ?  _ ⇒ ?]?)914 [2: whd in ⊢ (??%%)915 XXX916 *)917 918 (* axiom construct_costs_sigma:919 ∀p.∀pol:policy p.∀ppc,pc,costs,i.920 bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →921 bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).922 923 axiom tech_pc_sigma00_append_Some:924 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.925 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →926 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)927 605 928 606 axiom eq_identifier_eq: … … 1070 748 1071 749 (*CSC: move elsewhere *) 750 axiom nat_of_bitvector_add: 751 ∀n,v1,v2. 752 nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n → 753 nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2. 754 755 (*CSC: move elsewhere *) 1072 756 lemma fetch_pseudo_instruction_append: 1073 ∀l1,l2 ,ppc,ppc_ok,ppc_ok'.757 ∀l1,l2. l1@l2 < 2^16 → ∀ppc,ppc_ok,ppc_ok'. 1074 758 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 1075 759 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) ppc_ok' = 1076 760 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉. 1077 #l1 #l2 #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 1078 (*CSC: FALSE, NEED INVARIANT? *) 1079 > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (l1)) ppc) 1080 = l1 + nat_of_bitvector … ppc) [2: cases daemon] 761 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 762 cut (l1 + nat_of_bitvector … ppc < 2^16) 763 [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ] 764 l1l2_ok #l1ppc_ok >nat_of_bitvector_add 765 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 766 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 1081 767 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???) 1082 768 #lbl #instr normalize nodelta >add_associative % … … 1085 771 definition assembly: 1086 772 ∀p: pseudo_assembly_program. 773 \snd p < 2^16 → 1087 774 ∀sigma: Word → Word. 1088 775 ∀policy: Word → bool. … … 1103 790 assembled K 1104 791 ≝ 1105 λp. 792 λp. λinstr_list_ok. 1106 793 λsigma. 1107 794 λpolicy. … … 1141 828  % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 1142 829  cases ppc_code in p1; ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; EQppc_code 1143 * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]1144 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 830 * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)] 831 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc 1145 832 cases (le_to_or_lt_eq … LTppc') 1146 833 [2: #S_S_eq normalize nodelta in S_S_eq; 1147 834 (*CSC: FALSE, NEEDS INVARIANT *) 1148 cut (ppc' = ppc) [ cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' >prf1149 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc #Xlapply LTppc835 cut (ppc' = ppc) [ normalize nodelta in LTppc_ppc; >IH1 cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' >prf 836 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc 1150 837 >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → match % with [_ ⇒ ?]); 1151 838 >fetch_pseudo_instruction_append 1152 [3: @le_S_S @le_O_n 2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → ?); #H @H] 839 [3: @le_S_S @le_O_n 840 2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → ?); #H @H 841 4: <prf <p_refl in instr_list_ok; #H @H ] 1153 842 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 1154 #j #LTj 1155 (* CSC: FALSE, NEEDS INVARIANT *)1156 >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) =1157 nat_of_bitvector … (sigma ppc) + j) [2: cases daemon]843 #j #LTj >nat_of_bitvector_add 844 >nat_of_bitvector_bitvector_of_nat_inverse 845 [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon 846 3: (* CSC: TRUE, NEEDS INVARIANT *) cases daemon ] 1158 847 >reverse_append >reverse_reverse 1159 (* CSC: TRUE, NEEDS INVARIANT *)848 (* CSC: TRUE, NEEDS SAME INVARIANT *) 1160 849 >(? : nat_of_bitvector … (sigma ppc) = reverse … code) [2: cases daemon] 1161 850 @nth_safe_prepend 1162  #LTppc' #LT_ppc_ppc lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ] 851  #LTppc'' lapply (IH2 ppc' ?) 852 [ @(transitive_le … LTppc'') @le_S_S // ] 1163 853 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1164 854 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH … … 1166 856 >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K 1167 857 >IH 1168 [2: (*CSC: FALSE, NEEDS INVARIANT ? *) cases daemon858 [2: (*CSC: FALSE, NEEDS INVARIANT PPC'=PPC TO AVOID @PAIR_ELIM ABOVE? *) cases daemon 1169 859  @shift_nth_prefix 1170 860 3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
Note: See TracChangeset
for help on using the changeset viewer.