DEFINITION leq_trans()
TYPE =
∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(leq g a2 a3)→(leq g a1 a3)
BODY =
assume g: G
assume a1: A
assume a2: A
suppose H: leq g a1 a2
we proceed by induction on H to prove ∀a3:A.(leq g a2 a3)→(leq g a1 a3)
case leq_sort : h1:nat h2:nat n1:nat n2:nat k:nat H0:eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k) ⇒
the thesis becomes ∀a3:A.∀H1:(leq g (ASort h2 n2) a3).(leq g (ASort h1 n1) a3)
assume a3: A
suppose H1: leq g (ASort h2 n2) a3
(H_x)
by (leq_gen_sort1 . . . . H1)
ex2_3
nat
nat
nat
λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort h2 n2) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A a3 (ASort h2 n2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove leq g (ASort h1 n1) a3
case ex2_3_intro : x0:nat x1:nat x2:nat H3:eq A (aplus g (ASort h2 n2) x2) (aplus g (ASort x1 x0) x2) H4:eq A a3 (ASort x1 x0) ⇒
the thesis becomes leq g (ASort h1 n1) a3
(H5)
by (f_equal . . . . . H4)
we proved eq A a3 (ASort x1 x0)
eq A (λe:A.e a3) (λe:A.e (ASort x1 x0))
end of H5
(h1)
suppose H6: lt k x2
(H_y)
by (aplus_reg_r . . . . . H0 .)
eq
A
aplus g (ASort h1 n1) (plus (minus x2 k) k)
aplus g (ASort h2 n2) (plus (minus x2 k) k)
end of H_y
(H7)
(h1)
by (le_n .)
we proved le k k
by (le_S . . previous)
le k (S k)
end of h1
(h2)
consider H6
we proved lt k x2
le (S k) x2
end of h2
by (le_trans . . . h1 h2)
we proved le k x2
by (le_plus_minus_sym . . previous)
we proved eq nat x2 (plus (minus x2 k) k)
by (eq_ind_r . . . H_y . previous)
eq A (aplus g (ASort h1 n1) x2) (aplus g (ASort h2 n2) x2)
end of H7
by (trans_eq . . . . H7 H3)
we proved eq A (aplus g (ASort h1 n1) x2) (aplus g (ASort x1 x0) x2)
by (leq_sort . . . . . . previous)
we proved leq g (ASort h1 n1) (ASort x1 x0)
(lt k x2)→(leq g (ASort h1 n1) (ASort x1 x0))
end of h1
(h2)
suppose H6: le x2 k
(H_y)
by (aplus_reg_r . . . . . H3 .)
eq
A
aplus g (ASort h2 n2) (plus (minus k x2) x2)
aplus g (ASort x1 x0) (plus (minus k x2) x2)
end of H_y
(H7)
by (le_plus_minus_sym . . H6)
we proved eq nat k (plus (minus k x2) x2)
by (eq_ind_r . . . H_y . previous)
eq A (aplus g (ASort h2 n2) k) (aplus g (ASort x1 x0) k)
end of H7
by (trans_eq . . . . H0 H7)
we proved eq A (aplus g (ASort h1 n1) k) (aplus g (ASort x1 x0) k)
by (leq_sort . . . . . . previous)
we proved leq g (ASort h1 n1) (ASort x1 x0)
(le x2 k)→(leq g (ASort h1 n1) (ASort x1 x0))
end of h2
by (lt_le_e . . . h1 h2)
we proved leq g (ASort h1 n1) (ASort x1 x0)
by (eq_ind_r . . . previous . H5)
leq g (ASort h1 n1) a3
we proved leq g (ASort h1 n1) a3
∀a3:A.∀H1:(leq g (ASort h2 n2) a3).(leq g (ASort h1 n1) a3)
case leq_head : a3:A a4:A :leq g a3 a4 a5:A a6:A :leq g a5 a6 ⇒
the thesis becomes ∀a0:A.∀H4:(leq g (AHead a4 a6) a0).(leq g (AHead a3 a5) a0)
(H1) by induction hypothesis we know ∀a5:A.(leq g a4 a5)→(leq g a3 a5)
(H3) by induction hypothesis we know ∀a7:A.(leq g a6 a7)→(leq g a5 a7)
assume a0: A
suppose H4: leq g (AHead a4 a6) a0
(H_x)
by (leq_gen_head1 . . . . H4)
ex3_2 A A λa3:A.λ:A.leq g a4 a3 λ:A.λa4:A.leq g a6 a4 λa3:A.λa4:A.eq A a0 (AHead a3 a4)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove leq g (AHead a3 a5) a0
case ex3_2_intro : x0:A x1:A H6:leq g a4 x0 H7:leq g a6 x1 H8:eq A a0 (AHead x0 x1) ⇒
the thesis becomes leq g (AHead a3 a5) a0
(H9)
by (f_equal . . . . . H8)
we proved eq A a0 (AHead x0 x1)
eq A (λe:A.e a0) (λe:A.e (AHead x0 x1))
end of H9
(h1) by (H1 . H6) we proved leq g a3 x0
(h2) by (H3 . H7) we proved leq g a5 x1
by (leq_head . . . h1 . . h2)
we proved leq g (AHead a3 a5) (AHead x0 x1)
by (eq_ind_r . . . previous . H9)
leq g (AHead a3 a5) a0
we proved leq g (AHead a3 a5) a0
∀a0:A.∀H4:(leq g (AHead a4 a6) a0).(leq g (AHead a3 a5) a0)
we proved ∀a3:A.(leq g a2 a3)→(leq g a1 a3)
we proved ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(leq g a2 a3)→(leq g a1 a3)