Changeset 1516 for src/common/PositiveMap.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/PositiveMap.ma
r1515 r1516 62 62 [ * // 63 63  #tl #IH * 64 [ whd in ⊢ (??%%) @IH64 [ whd in ⊢ (??%%); @IH 65 65  #x #l #r @IH 66 66 ] 67 67  #tl #IH * 68 [ whd in ⊢ (??%%) @IH68 [ whd in ⊢ (??%%); @IH 69 69  #x #l #r @IH 70 70 ] … … 80 80  #b' #IH * 81 81 [ * [ #NE @refl  #x #l #r #NE @refl ] 82  #c' * [ #NE whd in ⊢ (??%%) @IH /2/83  #x #l #r #NE whd in ⊢ (??%%) @IH /2/82  #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 83  #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 84 84 ] 85 85  #c' * // … … 88 88 [ * [ #NE @refl  #x #l #r #NE @refl ] 89 89  #c' * // 90  #c' * [ #NE whd in ⊢ (??%%) @IH /2/91  #x #l #r #NE whd in ⊢ (??%%) @IH /2/90  #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 91  #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 92 92 ] 93 93 ] … … 110 110 [ * [ //  * // #x #l #r normalize #E destruct ] 111 111  #b' #IH * [ //  #x #l #r #U @IH whd in U:(??%?); 112 cases (update A b' a r) in U ⊢ % 112 cases (update A b' a r) in U ⊢ %; 113 113 [ //  normalize #t #E destruct ] 114 114 ] 115 115  #b' #IH * [ //  #x #l #r #U @IH whd in U:(??%?); 116 cases (update A b' a l) in U ⊢ % 116 cases (update A b' a l) in U ⊢ %; 117 117 [ //  normalize #t #E destruct ] 118 118 ] … … 124 124 #A #b #a elim b 125 125 [ * [ #t' normalize #E destruct 126  * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?) 126  * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?); 127 127 #E destruct // 128 128 ] 129 129  #b' #IH * 130 130 [ #t' normalize #E destruct 131  #x #l #r #t' whd in ⊢ (??%? → ??%?) 131  #x #l #r #t' whd in ⊢ (??%? → ??%?); 132 132 lapply (IH r) 133 133 cases (update A b' a r) … … 138 138  #b' #IH * 139 139 [ #t' normalize #E destruct 140  #x #l #r #t' whd in ⊢ (??%? → ??%?) 140  #x #l #r #t' whd in ⊢ (??%? → ??%?); 141 141 lapply (IH l) 142 142 cases (update A b' a l)
Note: See TracChangeset
for help on using the changeset viewer.