Changeset 1519 for src/ASM/Interpret.ma
 Timestamp:
 Nov 21, 2011, 12:10:57 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1515 r1519 40 40 # H2 41 41 normalize 42 change in H2: (??%?) with (orb ??)42 change in H2: (??%?); with (orb ??) 43 43 cases (inclusive_disjunction_true … H2) 44 44 [ # K … … 77 77 # tl 78 78 # II 79 whd in ⊢ (% → ? → ?) 79 whd in ⊢ (% → ? → ?); 80 80 lapply (refl … (is_in … (he:::tl) a)) 81 cases (is_in … (he:::tl) a) in ⊢ (???% → %) 81 cases (is_in … (he:::tl) a) in ⊢ (???% → %); 82 82 [ # K 83 83 # _ 84 84 normalize in K; 85 whd in ⊢ (% → ?) 86 lapply (refl … (subvector_with … eq_a (he:::tl) q)) 87 cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %) 85 whd in ⊢ (% → ?); 86 lapply (refl … (subvector_with … eq_a (he:::tl) q)); 87 cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %); 88 88 [ # K1 89 89 # _ 90 change in K1 with ((andb ? (subvector_with …)) = true)90 change in K1; with ((andb ? (subvector_with …)) = true) 91 91 cases (conjunction_true … K1) 92 92 # K3 … … 105 105  # K1 106 106 # K2 107 (normalize in K2 )107 (normalize in K2;) 108 108 cases K2; 109 109 ]
Note: See TracChangeset
for help on using the changeset viewer.