DEFINITION sc3_repl()
TYPE =
∀g:G.∀a1:A.∀c:C.∀t:T.(sc3 g a1 c t)→∀a2:A.(leq g a1 a2)→(sc3 g a2 c t)
BODY =
assume g: G
assume a1: A
assume a2: A
we proceed by induction on a2 to prove
∀a3:A.(llt a3 a2)→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g a2 c t)→∀a3:A.(leq g a2 a3)→(sc3 g a3 c t)
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀a3:A.(llt a3 (ASort n n0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g (ASort n n0) c t)→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
suppose :
∀a3:A.(llt a3 (ASort n n0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
assume c: C
assume t: T
we must prove (sc3 g (ASort n n0) c t)→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
or equivalently
land (arity g c t (ASort n n0)) (sn3 c t)
→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
suppose H0: land (arity g c t (ASort n n0)) (sn3 c t)
assume a3: A
suppose H1: leq g (ASort n n0) a3
(H2) consider H0
we proceed by induction on H2 to prove sc3 g a3 c t
case conj : H3:arity g c t (ASort n n0) H4:sn3 c t ⇒
the thesis becomes sc3 g a3 c t
(H_y)
by (arity_repl . . . . H3 . H1)
arity g c t a3
end of H_y
(H_x)
by (leq_gen_sort1 . . . . H1)
ex2_3
nat
nat
nat
λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort n n0) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A a3 (ASort h2 n2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove sc3 g a3 c t
case ex2_3_intro : x0:nat x1:nat x2:nat :eq A (aplus g (ASort n n0) x2) (aplus g (ASort x1 x0) x2) H7:eq A a3 (ASort x1 x0) ⇒
the thesis becomes sc3 g a3 c t
(H8)
by (f_equal . . . . . H7)
we proved eq A a3 (ASort x1 x0)
eq A (λe:A.e a3) (λe:A.e (ASort x1 x0))
end of H8
(H9)
we proceed by induction on H8 to prove arity g c t (ASort x1 x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H_y
arity g c t (ASort x1 x0)
end of H9
by (conj . . H9 H4)
we proved land (arity g c t (ASort x1 x0)) (sn3 c t)
that is equivalent to sc3 g (ASort x1 x0) c t
by (eq_ind_r . . . previous . H8)
sc3 g a3 c t
sc3 g a3 c t
we proved sc3 g a3 c t
we proved
land (arity g c t (ASort n n0)) (sn3 c t)
→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
that is equivalent to (sc3 g (ASort n n0) c t)→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
∀a3:A.(llt a3 (ASort n n0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g (ASort n n0) c t)→∀a3:A.(leq g (ASort n n0) a3)→(sc3 g a3 c t)
case AHead : a:A a0:A ⇒
the thesis becomes
∀H1:∀a3:A.(llt a3 (AHead a a0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
.∀c:C.∀t:T.(sc3 g (AHead a a0) c t)→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
() by induction hypothesis we know
∀a3:A.(llt a3 a)→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g a c t)→∀a3:A.(leq g a a3)→(sc3 g a3 c t)
(H0) by induction hypothesis we know
∀a3:A.(llt a3 a0)→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g a0 c t)→∀a3:A.(leq g a0 a3)→(sc3 g a3 c t)
suppose H1:
∀a3:A.(llt a3 (AHead a a0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
assume c: C
assume t: T
we must prove (sc3 g (AHead a a0) c t)→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
or equivalently
(land
arity g c t (AHead a a0)
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList.(drop1 is d c)→(sc3 g a0 d (THead (Flat Appl) w (lift1 is t))))
→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
suppose H2:
land
arity g c t (AHead a a0)
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList.(drop1 is d c)→(sc3 g a0 d (THead (Flat Appl) w (lift1 is t)))
assume a3: A
suppose H3: leq g (AHead a a0) a3
(H4) consider H2
we proceed by induction on H4 to prove sc3 g a3 c t
case conj : H5:arity g c t (AHead a a0) H6:∀d:C.∀w:T.(sc3 g a d w)→∀is:PList.(drop1 is d c)→(sc3 g a0 d (THead (Flat Appl) w (lift1 is t))) ⇒
the thesis becomes sc3 g a3 c t
(H_x)
by (leq_gen_head1 . . . . H3)
ex3_2 A A λa3:A.λ:A.leq g a a3 λ:A.λa4:A.leq g a0 a4 λa3:A.λa4:A.eq A a3 (AHead a3 a4)
end of H_x
(H7) consider H_x
we proceed by induction on H7 to prove sc3 g a3 c t
case ex3_2_intro : x0:A x1:A H8:leq g a x0 H9:leq g a0 x1 H10:eq A a3 (AHead x0 x1) ⇒
the thesis becomes sc3 g a3 c t
(H11)
by (f_equal . . . . . H10)
we proved eq A a3 (AHead x0 x1)
eq A (λe:A.e a3) (λe:A.e (AHead x0 x1))
end of H11
(h1)
by (leq_head . . . H8 . . H9)
we proved leq g (AHead a a0) (AHead x0 x1)
by (arity_repl . . . . H5 . previous)
arity g c t (AHead x0 x1)
end of h1
(h2)
assume d: C
assume w: T
suppose H12: sc3 g x0 d w
assume is: PList
suppose H13: drop1 is d c
(h1)
assume a4: A
suppose H14: llt a4 a0
assume c0: C
assume t0: T
suppose H15: sc3 g a4 c0 t0
assume a5: A
suppose H16: leq g a4 a5
by (llt_head_dx . .)
we proved llt a0 (AHead a a0)
by (llt_trans . . . H14 previous)
we proved llt a4 (AHead a a0)
by (H1 . previous . . H15 . H16)
we proved sc3 g a5 c0 t0
∀a4:A.(llt a4 a0)→∀c0:C.∀t0:T.(sc3 g a4 c0 t0)→∀a5:A.(leq g a4 a5)→(sc3 g a5 c0 t0)
end of h1
(h2)
(h1)
by (llt_head_sx . .)
we proved llt a (AHead a a0)
by (llt_repl . . . H8 . previous)
llt x0 (AHead a a0)
end of h1
(h2)
by (leq_sym . . . H8)
leq g x0 a
end of h2
by (H1 . h1 . . H12 . h2)
we proved sc3 g a d w
by (H6 . . previous . H13)
sc3 g a0 d (THead (Flat Appl) w (lift1 is t))
end of h2
by (H0 h1 . . h2 . H9)
we proved sc3 g x1 d (THead (Flat Appl) w (lift1 is t))
∀d:C
.∀w:T
.sc3 g x0 d w
→∀is:PList.(drop1 is d c)→(sc3 g x1 d (THead (Flat Appl) w (lift1 is t)))
end of h2
by (conj . . h1 h2)
we proved
land
arity g c t (AHead x0 x1)
∀d:C
.∀w:T
.sc3 g x0 d w
→∀is:PList.(drop1 is d c)→(sc3 g x1 d (THead (Flat Appl) w (lift1 is t)))
that is equivalent to sc3 g (AHead x0 x1) c t
by (eq_ind_r . . . previous . H11)
sc3 g a3 c t
sc3 g a3 c t
we proved sc3 g a3 c t
we proved
(land
arity g c t (AHead a a0)
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList.(drop1 is d c)→(sc3 g a0 d (THead (Flat Appl) w (lift1 is t))))
→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
that is equivalent to (sc3 g (AHead a a0) c t)→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
∀H1:∀a3:A.(llt a3 (AHead a a0))→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
.∀c:C.∀t:T.(sc3 g (AHead a a0) c t)→∀a3:A.(leq g (AHead a a0) a3)→(sc3 g a3 c t)
we proved
∀a3:A.(llt a3 a2)→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g a2 c t)→∀a3:A.(leq g a2 a3)→(sc3 g a3 c t)
we proved
∀a2:A
.∀a3:A.(llt a3 a2)→∀c:C.∀t:T.(sc3 g a3 c t)→∀a4:A.(leq g a3 a4)→(sc3 g a4 c t)
→∀c:C.∀t:T.(sc3 g a2 c t)→∀a3:A.(leq g a2 a3)→(sc3 g a3 c t)
by (llt_wf_ind . previous .)
we proved ∀c:C.∀t:T.(sc3 g a1 c t)→∀a2:A.(leq g a1 a2)→(sc3 g a2 c t)
we proved ∀g:G.∀a1:A.∀c:C.∀t:T.(sc3 g a1 c t)→∀a2:A.(leq g a1 a2)→(sc3 g a2 c t)