Changeset 3570 for LTS/Language.ma


Ignore:
Timestamp:
Jun 17, 2015, 5:49:19 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3561 r3570  
    8989lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,l_p,i1,i2.(i1 = i2 → P true) →
    9090(i1 ≠ i2 → P false) → P (eq_instructions p l_p i1 i2).
    91 #P #p #l_p #i1 elim i1
    92 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
     91#P #p #l_p #i1 lapply P -P elim i1
     92[ #P * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9393  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
    94 | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
     94| #rt #P * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
    9595  #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //]
    9696  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9797  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
    98 | #seq * [| #lbl] #i #IH * normalize
     98| #seq * [| #lbl] #i #IH #P * normalize
    9999  [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c
    100100  |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3]
Note: See TracChangeset for help on using the changeset viewer.