matita/matita/contribs/mf/de.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 definition eDe: est → est.
   6  #I %
   7  [ @(De I)
   8  | @De_rect_Type1
   9    [ #z @(z = c_unit …)
  10    | #i * [ 2: #i' @(i ≃ i') | 3,4: #_ #_ ] @falsum
  11    | #F1 #F2 #H1 #H2 * [ 3: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 4: #_ #_ ] @falsum
  12    | #F1 #F2 #H1 #H2 * [ 4: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 3: #_ #_ ] @falsum
  13    ]
  14  | %
  15    [ @De_rect_CProp0
  16      [ %
  17      | @rfl
  18      | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
  19      | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
  20      ]
  21    | @De_rect_CProp0
  22      [ * [ #_ % | #i #abs @(De_clash_unit_ev I i abs)
  23          | #F1 #F2 #abs @(De_clash_unit_times I F1 F2 abs)
  24          | #F1 #F2 #abs @(De_clash_unit_plus I F1 F2 abs) ]
  25      | #i * [ @falsum_rect_CProp0 | #i' @sym | 3,4: #F1' #F2' #abs @abs ]
  26      | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
  27                          | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ]
  28                          | #F1' #F2' #abs @abs ]
  29      | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
  30                          | #F1' #F2' #abs @abs
  31                          | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ] ]
  32      ]
  33    | @De_rect_CProp0
  34      [ * [ #F'' #_ #h @h
  35          | #i' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_ev I i' abs))
  36          | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_times I F1' F2' abs))
  37          | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_plus I F1' F2' abs))
  38          ]
  39      | #i * [ #F'' @falsum_rect_CProp0
  40             | #i' * [ #_ #abs @abs
  41                     | #i'' @tra
  42                     | 3,4: #F1'' #F2'' #_ #abs @abs
  43                     ]
  44             | 3,4: #F1' #F2' #F'' @falsum_rect_CProp0
  45             ]
  46      | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
  47                          | #i' #F'' @falsum_rect_CProp0
  48                          | #F1' #F2' * [ #_ #abs @abs
  49                                        | #i'' #_ #abs @abs
  50                                        | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
  51                                          [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
  52                                        | #F1'' #F2'' #_ #abs @abs
  53                                        ]
  54                          | #F1' #F2' #F'' @falsum_rect_CProp0
  55                          ]
  56      | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
  57                          | #i' #F'' @falsum_rect_CProp0
  58                          | #F1' #F2' #F'' @falsum_rect_CProp0
  59                          | #F1' #F2' * [ #_ #abs @abs
  60                                        | #i'' #_ #abs @abs
  61                                        | #F1'' #F2'' #_ #abs @abs
  62                                        | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
  63                                          [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
  64                                        ]
  65                          ]
  66      ]
  67    ]
  68  ]
  69 qed.
  70