Changeset 3561 for LTS/Language.ma
 Timestamp:
 Jun 16, 2015, 2:39:12 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3549 r3561 87 87 ]. 88 88 89 90 (* 91 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 92 (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). 93 #P #p #i1 elim i1 89 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,l_p,i1,i2.(i1 = i2 → P true) → 90 (i1 ≠ i2 → P false) → P (eq_instructions p l_p i1 i2). 91 #P #p #l_p #i1 elim i1 94 92 [* normalize [/2/ ] #x [*: #y #z [2,3: #w1 #w2 [#w3] 4,5: #w1]] #_ #H2 @H2 % #EQ 95 93 lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') … … 105 103 [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 106 104 >(\b (refl …)) in ABS; #EQ destruct] 107 #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2108 [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 109 *) 105 #EQseq cases daemon 106 *: cases daemon 107 qed. 110 108 111 109 record env_params : Type[1] ≝
Note: See TracChangeset
for help on using the changeset viewer.