Changeset 1948 for src/ASM/Interpret.ma
 Timestamp:
 May 15, 2012, 11:13:14 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1946 r1948 8 8 let b ≝ get_index_v ? 8 c 1 ? in 9 9 [[ b; b; b; b; b; b; b; b ]] @@ c. 10 normalize ;11 repeat (@ (le_S_S ?));12 @ (le_O_n);10 normalize 11 repeat (@le_S_S) 12 @le_O_n 13 13 qed. 14 14 15 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.16 # a17 # b18 cases a19 cases b15 lemma eq_a_to_eq: 16 ∀a,b. 17 eq_a a b = true → a = b. 18 #a #b 19 cases a cases b 20 20 normalize 21 # 21 #K 22 22 try % 23 23 cases (eq_true_false K) … … 25 25 26 26 lemma is_a_to_mem_to_is_in: 27 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 28 # he 29 # a 30 # m 31 # q 27 ∀he,a,m,q. 28 is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 29 #he #a #m #q 32 30 elim q 33 [ normalize 34 # _ 35 # K 36 assumption 37  # m' 38 # t 39 # q' 40 # II 41 # H1 42 # H2 31 [1: 32 #_ #K assumption 33 2: 34 #m' #t #q' #II #H1 #H2 43 35 normalize 44 change with (orb ??) in H2: 36 change with (orb ??) in H2:(??%?); 45 37 cases (inclusive_disjunction_true … H2) 46 [ # K47 < (eq_a_to_eq … K)48 > H149 %50  #K51 > 38 [1: 39 #K 40 <(eq_a_to_eq … K) >H1 % 41 2: 42 #K 43 >II 52 44 try assumption 53 45 cases (is_a t a)
Note: See TracChangeset
for help on using the changeset viewer.