Changeset 3561 for LTS/Language.ma


Ignore:
Timestamp:
Jun 16, 2015, 2:39:12 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3549 r3561  
    8787].
    8888
    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
     89lemma 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
    9492[* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9593  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
     
    105103  [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    106104        >(\b (refl …)) in ABS; #EQ destruct]
    107   #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2
    108   [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    109 *)
     105  #EQseq cases daemon
     106|*: cases daemon
     107qed.
    110108
    111109record env_params : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.