matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_1a.etc

   1 (* FROM BASIC_1
   2
   3 (* NOTE: This can be generalized removing the last premise *)
   4       Lemma ty3_gen_cvoid: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
   5                            (e:?; u:?; d:?) (getl d c (CHead e (Bind Void) u)) ->
   6                            (a:?) (drop (1) d c a) ->
   7                            (EX y1 y2 | t1 = (lift (1) d y1) &
   8                                        t2 = (lift (1) d y2) &
   9                                        (ty3 g a y1 y2)
  10                            ).
  11
  12 Lemma ty3_gen_appl_nf2: (g:?; c:?; w,v,x:?) (ty3 g c (THead (Flat Appl) w v) x) ->
  13                         (EX u t | (pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x) &
  14                                   (ty3 g c v (THead (Bind Abst) u t)) &
  15                                   (ty3 g c w u) &
  16                                   (nf2 c (THead (Bind Abst) u t))
  17                         ).
  18
  19 Lemma ty3_arity: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
  20                  (EX a1 | (arity g c t1 a1) &
  21                           (arity g c t2 (asucc g a1))
  22                  ).
  23
  24 Lemma ty3_acyclic: (g:?; c:?; t,u:?)
  25                    (ty3 g c t u) -> (pc3 c u t) -> (P:Prop) P.
  26
  27 Theorem pc3_abst_dec: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
  28                       (u2,t2:?) (ty3 g c u2 t2) ->
  29                       (EX u v2 | (pc3 c u1 (THead (Bind Abst) u2 u)) &
  30                                  (ty3 g c (THead (Bind Abst) v2 u) t1) &
  31                                  (pr3 c u2 v2) & (nf2 c v2)
  32                       ) \/
  33                       ((u:?) (pc3 c u1 (THead (Bind Abst) u2 u)) -> False).
  34
  35 file ty3_nf2_gen
  36
  37 *)