DEFINITION arity_lift()
TYPE =
∀g:G
.∀c2:C
.∀t:T
.∀a:A
.arity g c2 t a
→∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c2)→(arity g c1 (lift h d t) a)
BODY =
assume g: G
assume c2: C
assume t: T
assume a: A
suppose H: arity g c2 t a
we proceed by induction on H to prove ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c2)→(arity g c1 (lift h d t) a)
case arity_sort : c:C n:nat ⇒
the thesis becomes
∀c1:C
.∀h:nat
.∀d:nat
.(drop h d c1 c)→(arity g c1 (lift h d (TSort n)) (ASort O n))
assume c1: C
assume h: nat
assume d: nat
suppose : drop h d c1 c
(h1)
by (arity_sort . . .)
arity g c1 (TSort n) (ASort O n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d (TSort n)) (ASort O n)
∀c1:C
.∀h:nat
.∀d:nat
.(drop h d c1 c)→(arity g c1 (lift h d (TSort n)) (ASort O n))
case arity_abbr : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) a0:A H1:arity g d u a0 ⇒
the thesis becomes ∀c1:C.∀h:nat.∀d0:nat.∀H3:(drop h d0 c1 c).(arity g c1 (lift h d0 (TLRef i)) a0)
(H2) by induction hypothesis we know ∀c1:C.∀h:nat.∀d0:nat.(drop h d0 c1 d)→(arity g c1 (lift h d0 u) a0)
assume c1: C
assume h: nat
assume d0: nat
suppose H3: drop h d0 c1 c
(h1)
suppose H4: lt i d0
(h1)
(H5)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_S . . previous)
we proved le (S i) (S d0)
by (le_S_n . . previous)
we proved le i d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop i O c1 e0
λe0:C.λe1:C.drop h (minus d0 i) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abbr) u)
end of H5
we proceed by induction on H5 to prove arity g c1 (TLRef i) a0
case ex3_2_intro : x0:C x1:C H6:drop i O c1 x0 H7:drop h (minus d0 i) x0 x1 H8:clear x1 (CHead d (Bind Abbr) u) ⇒
the thesis becomes arity g c1 (TLRef i) a0
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 i) (S (minus d0 (S i)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S i))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S i))) x0 x1
end of H9
(H10)
by (drop_clear_S . . . . H9 . . . H8)
ex2
C
λc1:C.clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S i)) u))
λc1:C.drop h (minus d0 (S i)) c1 d
end of H10
we proceed by induction on H10 to prove arity g c1 (TLRef i) a0
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) u)) H12:drop h (minus d0 (S i)) x d ⇒
the thesis becomes arity g c1 (TLRef i) a0
(h1)
by (getl_intro . . . . H6 H11)
getl i c1 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) u))
end of h1
(h2)
by (H2 . . . H12)
arity g x (lift h (minus d0 (S i)) u) a0
end of h2
by (arity_abbr . . . . . h1 . h2)
arity g c1 (TLRef i) a0
arity g c1 (TLRef i) a0
arity g c1 (TLRef i) a0
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
(lt i d0)→(arity g c1 (lift h d0 (TLRef i)) a0)
end of h1
(h2)
suppose H4: le d0 i
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus i h) c1 (CHead d (Bind Abbr) u)
by (arity_abbr . . . . . previous . H1)
arity g c1 (TLRef (plus i h)) a0
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef (plus i h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
(le d0 i)→(arity g c1 (lift h d0 (TLRef i)) a0)
end of h2
by (lt_le_e . . . h1 h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
∀c1:C.∀h:nat.∀d0:nat.∀H3:(drop h d0 c1 c).(arity g c1 (lift h d0 (TLRef i)) a0)
case arity_abst : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abst) u) a0:A H1:arity g d u (asucc g a0) ⇒
the thesis becomes ∀c1:C.∀h:nat.∀d0:nat.∀H3:(drop h d0 c1 c).(arity g c1 (lift h d0 (TLRef i)) a0)
(H2) by induction hypothesis we know ∀c1:C.∀h:nat.∀d0:nat.(drop h d0 c1 d)→(arity g c1 (lift h d0 u) (asucc g a0))
assume c1: C
assume h: nat
assume d0: nat
suppose H3: drop h d0 c1 c
(h1)
suppose H4: lt i d0
(h1)
(H5)
consider H4
we proved lt i d0
that is equivalent to le (S i) d0
by (le_S . . previous)
we proved le (S i) (S d0)
by (le_S_n . . previous)
we proved le i d0
by (drop_getl_trans_le . . previous . . . H3 . H0)
ex3_2
C
C
λe0:C.λ:C.drop i O c1 e0
λe0:C.λe1:C.drop h (minus d0 i) e0 e1
λ:C.λe1:C.clear e1 (CHead d (Bind Abst) u)
end of H5
we proceed by induction on H5 to prove arity g c1 (TLRef i) a0
case ex3_2_intro : x0:C x1:C H6:drop i O c1 x0 H7:drop h (minus d0 i) x0 x1 H8:clear x1 (CHead d (Bind Abst) u) ⇒
the thesis becomes arity g c1 (TLRef i) a0
(H9)
by (minus_x_Sy . . H4)
we proved eq nat (minus d0 i) (S (minus d0 (S i)))
we proceed by induction on the previous result to prove drop h (S (minus d0 (S i))) x0 x1
case refl_equal : ⇒
the thesis becomes the hypothesis H7
drop h (S (minus d0 (S i))) x0 x1
end of H9
(H10)
by (drop_clear_S . . . . H9 . . . H8)
ex2
C
λc1:C.clear x0 (CHead c1 (Bind Abst) (lift h (minus d0 (S i)) u))
λc1:C.drop h (minus d0 (S i)) c1 d
end of H10
we proceed by induction on H10 to prove arity g c1 (TLRef i) a0
case ex_intro2 : x:C H11:clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u)) H12:drop h (minus d0 (S i)) x d ⇒
the thesis becomes arity g c1 (TLRef i) a0
(h1)
by (getl_intro . . . . H6 H11)
getl i c1 (CHead x (Bind Abst) (lift h (minus d0 (S i)) u))
end of h1
(h2)
by (H2 . . . H12)
arity g x (lift h (minus d0 (S i)) u) (asucc g a0)
end of h2
by (arity_abst . . . . . h1 . h2)
arity g c1 (TLRef i) a0
arity g c1 (TLRef i) a0
arity g c1 (TLRef i) a0
end of h1
(h2)
by (lift_lref_lt . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef i)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
(lt i d0)→(arity g c1 (lift h d0 (TLRef i)) a0)
end of h1
(h2)
suppose H4: le d0 i
(h1)
by (drop_getl_trans_ge . . . . . H3 . H0 H4)
we proved getl (plus i h) c1 (CHead d (Bind Abst) u)
by (arity_abst . . . . . previous . H1)
arity g c1 (TLRef (plus i h)) a0
end of h1
(h2)
by (lift_lref_ge . . . H4)
eq T (lift h d0 (TLRef i)) (TLRef (plus i h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
(le d0 i)→(arity g c1 (lift h d0 (TLRef i)) a0)
end of h2
by (lt_le_e . . . h1 h2)
we proved arity g c1 (lift h d0 (TLRef i)) a0
∀c1:C.∀h:nat.∀d0:nat.∀H3:(drop h d0 c1 c).(arity g c1 (lift h d0 (TLRef i)) a0)
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g (CHead c (Bind b) u) t0 a2 ⇒
the thesis becomes ∀c1:C.∀h:nat.∀d:nat.∀H5:(drop h d c1 c).(arity g c1 (lift h d (THead (Bind b) u t0)) a2)
(H2) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d u) a1)
(H4) by induction hypothesis we know
∀c1:C
.∀h:nat
.∀d:nat.(drop h d c1 (CHead c (Bind b) u))→(arity g c1 (lift h d t0) a2)
assume c1: C
assume h: nat
assume d: nat
suppose H5: drop h d c1 c
(h1)
(h1)
by (H2 . . . H5)
arity g c1 (lift h d u) a1
end of h1
(h2)
by (drop_skip_bind . . . . H5 . .)
we proved
drop
h
S d
CHead c1 (Bind b) (lift h d u)
CHead c (Bind b) u
that is equivalent to
drop
h
s (Bind b) d
CHead c1 (Bind b) (lift h d u)
CHead c (Bind b) u
by (H4 . . . previous)
arity
g
CHead c1 (Bind b) (lift h d u)
lift h (s (Bind b) d) t0
a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
arity
g
c1
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)
a2
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) u t0)
THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d (THead (Bind b) u t0)) a2
∀c1:C.∀h:nat.∀d:nat.∀H5:(drop h d c1 c).(arity g c1 (lift h d (THead (Bind b) u t0)) a2)
case arity_head : c:C u:T a1:A :arity g c u (asucc g a1) t0:T a2:A :arity g (CHead c (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀c1:C
.∀h:nat
.∀d:nat
.∀H4:drop h d c1 c
.arity g c1 (lift h d (THead (Bind Abst) u t0)) (AHead a1 a2)
(H1) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d u) (asucc g a1))
(H3) by induction hypothesis we know
∀c1:C
.∀h:nat
.∀d:nat
.(drop h d c1 (CHead c (Bind Abst) u))→(arity g c1 (lift h d t0) a2)
assume c1: C
assume h: nat
assume d: nat
suppose H4: drop h d c1 c
(h1)
(h1)
by (H1 . . . H4)
arity g c1 (lift h d u) (asucc g a1)
end of h1
(h2)
by (drop_skip_bind . . . . H4 . .)
we proved
drop
h
S d
CHead c1 (Bind Abst) (lift h d u)
CHead c (Bind Abst) u
that is equivalent to
drop
h
s (Bind Abst) d
CHead c1 (Bind Abst) (lift h d u)
CHead c (Bind Abst) u
by (H3 . . . previous)
arity
g
CHead c1 (Bind Abst) (lift h d u)
lift h (s (Bind Abst) d) t0
a2
end of h2
by (arity_head . . . . h1 . . h2)
arity
g
c1
THead (Bind Abst) (lift h d u) (lift h (s (Bind Abst) d) t0)
AHead a1 a2
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind Abst) u t0)
THead (Bind Abst) (lift h d u) (lift h (s (Bind Abst) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d (THead (Bind Abst) u t0)) (AHead a1 a2)
∀c1:C
.∀h:nat
.∀d:nat
.∀H4:drop h d c1 c
.arity g c1 (lift h d (THead (Bind Abst) u t0)) (AHead a1 a2)
case arity_appl : c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g c t0 (AHead a1 a2) ⇒
the thesis becomes
∀c1:C
.∀h:nat
.∀d:nat.∀H4:(drop h d c1 c).(arity g c1 (lift h d (THead (Flat Appl) u t0)) a2)
(H1) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d u) a1)
(H3) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d t0) (AHead a1 a2))
assume c1: C
assume h: nat
assume d: nat
suppose H4: drop h d c1 c
(h1)
(h1)
by (H1 . . . H4)
arity g c1 (lift h d u) a1
end of h1
(h2)
consider H4
we proved drop h d c1 c
that is equivalent to drop h (s (Flat Appl) d) c1 c
by (H3 . . . previous)
arity g c1 (lift h (s (Flat Appl) d) t0) (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
arity
g
c1
THead (Flat Appl) (lift h d u) (lift h (s (Flat Appl) d) t0)
a2
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Appl) u t0)
THead (Flat Appl) (lift h d u) (lift h (s (Flat Appl) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d (THead (Flat Appl) u t0)) a2
∀c1:C
.∀h:nat
.∀d:nat.∀H4:(drop h d c1 c).(arity g c1 (lift h d (THead (Flat Appl) u t0)) a2)
case arity_cast : c:C u:T a0:A :arity g c u (asucc g a0) t0:T :arity g c t0 a0 ⇒
the thesis becomes
∀c1:C
.∀h:nat
.∀d:nat.∀H4:(drop h d c1 c).(arity g c1 (lift h d (THead (Flat Cast) u t0)) a0)
(H1) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d u) (asucc g a0))
(H3) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d t0) a0)
assume c1: C
assume h: nat
assume d: nat
suppose H4: drop h d c1 c
(h1)
(h1)
by (H1 . . . H4)
arity g c1 (lift h d u) (asucc g a0)
end of h1
(h2)
consider H4
we proved drop h d c1 c
that is equivalent to drop h (s (Flat Cast) d) c1 c
by (H3 . . . previous)
arity g c1 (lift h (s (Flat Cast) d) t0) a0
end of h2
by (arity_cast . . . . h1 . h2)
arity
g
c1
THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) t0)
a0
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat Cast) u t0)
THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved arity g c1 (lift h d (THead (Flat Cast) u t0)) a0
∀c1:C
.∀h:nat
.∀d:nat.∀H4:(drop h d c1 c).(arity g c1 (lift h d (THead (Flat Cast) u t0)) a0)
case arity_repl : c:C t0:T a1:A :arity g c t0 a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀c1:C.∀h:nat.∀d:nat.∀H3:(drop h d c1 c).(arity g c1 (lift h d t0) a2)
(H1) by induction hypothesis we know ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c)→(arity g c1 (lift h d t0) a1)
assume c1: C
assume h: nat
assume d: nat
suppose H3: drop h d c1 c
by (H1 . . . H3)
we proved arity g c1 (lift h d t0) a1
by (arity_repl . . . . previous . H2)
we proved arity g c1 (lift h d t0) a2
∀c1:C.∀h:nat.∀d:nat.∀H3:(drop h d c1 c).(arity g c1 (lift h d t0) a2)
we proved ∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c2)→(arity g c1 (lift h d t) a)
we proved
∀g:G
.∀c2:C
.∀t:T
.∀a:A
.arity g c2 t a
→∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c2)→(arity g c1 (lift h d t) a)