Require Import MyTactics. Require Import LambdaCalculusSyntax. Require Import LambdaCalculusValues. Require Import LambdaCalculusReduction. Require Import STLCDefinition. Require Import STLCLemmas.
This is a failed attempt to prove the lemma jt_te_substitution_0
in
a direct way, without introducing the auxiliary judgement js
. See
STLCLemmas for a valid proof.
forall (Delta : tyenv) (t1 : term) (U : ty), jt Delta t1 U -> forall (Gamma : var -> ty) (t2 : term) (T : ty), Delta = T .: Gamma -> jt Gamma t2 T -> jt Gamma t1.[t2/] U(* Let us attempt to naively prove this statement by induction. *)forall (Delta : tyenv) (t1 : term) (U : ty), jt Delta t1 U -> forall (Gamma : var -> ty) (t2 : term) (T : ty), Delta = T .: Gamma -> jt Gamma t2 T -> jt Gamma t1.[t2/] Ux:varGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)t:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)]) (TyFun T U)t1, t2:termT, U:tyGamma0:var -> tyT0:tyIHjt2:forall (Gamma : var -> ty) (t3 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t3 T1 -> jt Gamma t2.[t3/] TIHjt1:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t1.[t2/] (TyFun T U)H0:jt (T0 .: Gamma0) t2 TH:jt (T0 .: Gamma0) t1 (TyFun T U)t0:termH2:jt Gamma0 t0 T0jt Gamma0 (App t1.[t0/] t2.[t0/]) U(* JTVar. *)x:varGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)t1, t2:termT, U:tyGamma0:var -> tyT0:tyIHjt2:forall (Gamma : var -> ty) (t3 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t3 T1 -> jt Gamma t2.[t3/] TIHjt1:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t1.[t2/] (TyFun T U)H0:jt (T0 .: Gamma0) t2 TH:jt (T0 .: Gamma0) t1 (TyFun T U)t0:termH2:jt Gamma0 t0 T0jt Gamma0 (App t1.[t0/] t2.[t0/]) Ut:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)]) (TyFun T U)x:varGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) x) ((T0 .: Gamma0) x)Gamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) 0) ((T0 .: Gamma0) 0)x:natGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x))Gamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) 0) ((T0 .: Gamma0) 0)eauto.Gamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 t2 T0x:natGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x))x:natGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 ((t2 .: ids) (S x)) ((T0 .: Gamma0) (S x))eauto with jt. }x:natGamma0:var -> tyt2:termT0:tyH1:jt Gamma0 t2 T0jt Gamma0 (ids x) (Gamma0 x)(* JTApp. *) (* This case just works, thanks to the induction hypotheses. *)t1, t2:termT, U:tyGamma0:var -> tyT0:tyIHjt2:forall (Gamma : var -> ty) (t3 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t3 T1 -> jt Gamma t2.[t3/] TIHjt1:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t1.[t2/] (TyFun T U)H0:jt (T0 .: Gamma0) t2 TH:jt (T0 .: Gamma0) t1 (TyFun T U)t0:termH2:jt Gamma0 t0 T0jt Gamma0 (App t1.[t0/] t2.[t0/]) Ut:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)]) (TyFun T U)eauto with jt.t1, t2:termT, U:tyGamma0:var -> tyT0:tyIHjt2:forall (Gamma : var -> ty) (t3 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t3 T1 -> jt Gamma t2.[t3/] TIHjt1:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t1.[t2/] (TyFun T U)H0:jt (T0 .: Gamma0) t2 TH:jt (T0 .: Gamma0) t1 (TyFun T U)t0:termH2:jt Gamma0 t0 T0jt Gamma0 (App t1.[t0/] t2.[t0/]) U(* JTLam. *)t:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)]) (TyFun T U)t:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt Gamma0 (Lam t.[ids 0 .: lift 1 t2 .: ren (+1)]) (TyFun T U)(* We would now like to apply the induction hypothesis, but this fails, because the statement of the lemma allows substituting a term for variable 0, but we are now attempting to substitute a term for variable 1. *)t:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt (T .: Gamma0) t.[ids 0 .: lift 1 t2 .: ren (+1)] U(* The moral of the story is that it is preferable to state a lemma that allows applying an arbitrary substitution (of terms for term variables) to a term. This will give rise to statements that are more general, therefore both more powerful and easier to read. See STLCLemmas. *) Abort.t:termT, U:tyGamma0:var -> tyT0:tyIHjt:forall (Gamma : var -> ty) (t2 : term) (T1 : ty), T .: T0 .: Gamma0 = T1 .: Gamma -> jt Gamma t2 T1 -> jt Gamma t.[t2/] UH:jt (T .: T0 .: Gamma0) t Ut2:termH1:jt Gamma0 t2 T0jt (T .: Gamma0) t.[ids 0 .: lift 1 t2 .: ren (+1)] U
The subject reduction theorem, also known as type preservation: the typing judgement is preserved by one step of reduction.
This is proved here for cbv
, but could be proved for other notions
of reduction, such as cbn
, or strong reduction.
forall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> forall t' : term, cbv t t' -> jt Gamma t' T(* By induction on the type derivation, then by cases on `cbv t t'`. *)forall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> forall t' : term, cbv t t' -> jt Gamma t' T(* Case: JApp/RedBetaV. *)Gamma:tyenvt2:termT, U:tyt:termH:jt Gamma (Lam t) (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv (Lam t) t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jt Gamma t.[t2/] UGamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jt Gamma (App t3 t2) UGamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jt Gamma (App t1 u2) UGamma:tyenvt2:termT, U:tyt:termH:jt Gamma (Lam t) (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv (Lam t) t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2jt Gamma t.[t2/] Ueauto using jt_te_substitution_0.Gamma:tyenvt2:termT, U:tyt:termH0:jt Gamma t2 TIHjt1:forall t' : term, cbv (Lam t) t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' TH4:cbv_mask RuleBetaVH5:is_value t2H6:jt (T .: Gamma) t Ujt Gamma t.[t2/] U(* Case: JApp/RedAppL. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jt Gamma (App t3 t2) UGamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jt Gamma (App t1 u2) Ueauto with jt.Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tt3:termH4:cbv_mask RuleAppLH6:cbv t1 t3jt Gamma (App t3 t2) U(* Case: JApp/RedAppVR. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jt Gamma (App t1 u2) Ueauto with jt. } Qed.Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:forall t' : term, cbv t1 t' -> jt Gamma t' (TyFun T U)IHjt2:forall t' : term, cbv t2 t' -> jt Gamma t' Tu2:termH4:cbv_mask RuleAppVRH5:is_value t1H7:cbv t2 u2jt Gamma (App t1 u2) U
An inversion lemma: if a closed value admits a function type TyFun T1 T2
,
then it must be a lambda-abstraction.
forall (Gamma : tyenv) (t : term) (T1 T2 : ty), jt Gamma t (TyFun T1 T2) -> closed t -> is_value t -> exists t' : {bind term}, t = Lam t'(* By cases. The type system is so simple that an induction is not even required here. An induction would be required if the type system had non-syntax-directed rules, such as a subtyping rule, or type abstraction and type instantiation rules, as in System F. *)forall (Gamma : tyenv) (t : term) (T1 T2 : ty), jt Gamma t (TyFun T1 T2) -> closed t -> is_value t -> exists t' : {bind term}, t = Lam t'(* Case: JVar. A variable is not closed. Contradiction. *)Gamma:tyenvT1, T2:tyx:varH:jt Gamma (Var x) (TyFun T1 T2)H0:Gamma x = TyFun T1 T2H4:closed (Var x)H5:is_value (Var x)exists t' : {bind term}, Var x = Lam t'Gamma:tyenvT1, T2:tyt0:termH:jt Gamma (Lam t0) (TyFun T1 T2)H3:jt (T1 .: Gamma) t0 T2H5:closed (Lam t0)H6:is_value (Lam t0)exists t' : {bind term}, Lam t0 = Lam t'Gamma:tyenvT1, T2:tyt1, t2:termH:jt Gamma (App t1 t2) (TyFun T1 T2)T:tyH0:jt Gamma t1 (TyFun T (TyFun T1 T2))H1:jt Gamma t2 TH5:closed (App t1 t2)H6:is_value (App t1 t2)exists t' : {bind term}, App t1 t2 = Lam t'Gamma:tyenvT1, T2:tyx:varH:jt Gamma (Var x) (TyFun T1 T2)H0:Gamma x = TyFun T1 T2H4:closed (Var x)H5:is_value (Var x)exists t' : {bind term}, Var x = Lam t'eauto with closed.Gamma:tyenvT1, T2:tyx:varH:jt Gamma (Var x) (TyFun T1 T2)H0:Gamma x = TyFun T1 T2H4:closed (Var x)H5:is_value (Var x)False(* Case: JLam. Immediate. *)Gamma:tyenvT1, T2:tyt0:termH:jt Gamma (Lam t0) (TyFun T1 T2)H3:jt (T1 .: Gamma) t0 T2H5:closed (Lam t0)H6:is_value (Lam t0)exists t' : {bind term}, Lam t0 = Lam t'Gamma:tyenvT1, T2:tyt1, t2:termH:jt Gamma (App t1 t2) (TyFun T1 T2)T:tyH0:jt Gamma t1 (TyFun T (TyFun T1 T2))H1:jt Gamma t2 TH5:closed (App t1 t2)H6:is_value (App t1 t2)exists t' : {bind term}, App t1 t2 = Lam t'obvious.Gamma:tyenvT1, T2:tyt0:termH:jt Gamma (Lam t0) (TyFun T1 T2)H3:jt (T1 .: Gamma) t0 T2H5:closed (Lam t0)H6:is_value (Lam t0)exists t' : {bind term}, Lam t0 = Lam t'(* Case: JApp. An application is not a value. Contradiction. *)Gamma:tyenvT1, T2:tyt1, t2:termH:jt Gamma (App t1 t2) (TyFun T1 T2)T:tyH0:jt Gamma t1 (TyFun T (TyFun T1 T2))H1:jt Gamma t2 TH5:closed (App t1 t2)H6:is_value (App t1 t2)exists t' : {bind term}, App t1 t2 = Lam t'Gamma:tyenvT1, T2:tyt1, t2:termH:jt Gamma (App t1 t2) (TyFun T1 T2)T:tyH0:jt Gamma t1 (TyFun T (TyFun T1 T2))H1:jt Gamma t2 TH5:closed (App t1 t2)H6:is_value (App t1 t2)exists t' : {bind term}, App t1 t2 = Lam t'obvious. } Qed.Gamma:tyenvT1, T2:tyt1, t2:termH:jt Gamma (App t1 t2) (TyFun T1 T2)T:tyH0:jt Gamma t1 (TyFun T (TyFun T1 T2))H1:jt Gamma t2 TH5:closed (App t1 t2)H6:is_value (App t1 t2)False
The progress theorem: a closed, well-typed term must either be able to make one step of reduction or be a value.
forall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> closed t -> (exists t' : term, cbv t t') \/ is_value tforall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> closed t -> (exists t' : term, cbv t t') \/ is_value t(* By induction on the type derivation. *)forall (Gamma : tyenv) (t : term) (T : ty), jt Gamma t T -> closed t -> (exists t' : term, cbv t t') \/ is_value t(* Case: JVar. *)Gamma:var -> tyx:varH0:closed (Var x)(exists t' : term, cbv (Var x) t') \/ is_value (Var x)Gamma:var -> tyt:termT, U:tyH:jt (T .: Gamma) t UIHjt:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjt2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* A variable does not reduce, so we must find a contradiction among our hypotheses. Here, the hypothesis that `t` is closed provides such a contradiction. (We could also exploit the fact that, according to our definition of `is_value`, a variable is a value, but it is preferable not to do so if we can avoid it.) *)Gamma:var -> tyx:varH0:closed (Var x)(exists t' : term, cbv (Var x) t') \/ is_value (Var x)eauto with closed.Gamma:var -> tyx:varH0:closed (Var x)False(* Case: JLam. *)Gamma:var -> tyt:termT, U:tyH:jt (T .: Gamma) t UIHjt:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjt2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)obvious.Gamma:var -> tyt:termT, U:tyH:jt (T .: Gamma) t UIHjt:closed t -> (exists t' : term, cbv t t') \/ is_value tH0:closed (Lam t)(exists t' : term, cbv (Lam t) t') \/ is_value (Lam t)(* Case: JApp. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjt2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* Apply the induction hypothesis to `t1`. If `t1` reduces, then obviously `App t1 t2` reduces as well, so we are finished. There remains to consider the case where `t1` is a value. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt1:closed t1 -> (exists t' : term, cbv t1 t') \/ is_value t1IHjt2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* Reason in the same way about `t2`. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TIHjt2:closed t2 -> (exists t' : term, cbv t2 t') \/ is_value t2H1:closed (App t1 t2)H2:is_value t1(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* We wish to prove that `App t1 t2` is a beta-redex. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2(exists t' : term, cbv (App t1 t2) t') \/ is_value (App t1 t2)(* Because `t1` is a closed value and has a function type, it must be a lambda-abstraction. *)Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2exists t' : term, cbv (App t1 t2) t'Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2fact:=exists t' : {bind term}, t1 = Lam t':Propclosed t1Gamma:tyenvt2:termT, U:tyx:{bind term}H:jt Gamma (Lam x) (TyFun T U)H0:jt Gamma t2 TH2:is_value (Lam x)H1:closed (App (Lam x) t2)H3:is_value t2exists t' : term, cbv (App (Lam x) t2) t'eauto with closed.Gamma:tyenvt1, t2:termT, U:tyH:jt Gamma t1 (TyFun T U)H0:jt Gamma t2 TH1:closed (App t1 t2)H2:is_value t1H3:is_value t2fact:=exists t' : {bind term}, t1 = Lam t':Propclosed t1(* Therefore, we have a beta-redex. *) obvious. } Qed.Gamma:tyenvt2:termT, U:tyx:{bind term}H:jt Gamma (Lam x) (TyFun T U)H0:jt Gamma t2 TH2:is_value (Lam x)H1:closed (App (Lam x) t2)H3:is_value t2exists t' : term, cbv (App (Lam x) t2) t'