(* *)
(**************************************************************************)
-include "Basic_2/reducibility/trf.ma".
+include "basic_2/reducibility/trf.ma".
(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
-definition tif: predicate term โ ฮปT. ๐[T] โ False.
+definition tif: predicate term โ ฮปT. ๐โฆTโฆ โ โฅ.
interpretation "context-free irreducibility (term)"
'NotReducible T = (tif T).
(* Basic inversion lemmas ***************************************************)
-lemma tif_inv_abbr: โV,T. ๐[โV.T] โ False.
+lemma tif_inv_abbr: โV,T. ๐โฆโV.Tโฆ โ โฅ.
/2 width=1/ qed-.
-lemma tif_inv_abst: โV,T. ๐[โV.T] โ ๐[V] โง ๐[T].
+lemma tif_inv_abst: โV,T. ๐โฆโV.Tโฆ โ ๐โฆVโฆ โง ๐โฆTโฆ.
/4 width=1/ qed-.
-lemma tif_inv_appl: โV,T. ๐[โV.T] โ โงโง ๐[V] & ๐[T] & ๐[T].
+lemma tif_inv_appl: โV,T. ๐โฆโV.Tโฆ โ โงโง ๐โฆVโฆ & ๐โฆTโฆ & ๐โฆTโฆ.
#V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
-lemma tif_inv_cast: โV,T. ๐[โฃV.T] โ False.
+lemma tif_inv_cast: โV,T. ๐โฆโฃV.Tโฆ โ โฅ.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
-lemma tif_atom: โI. ๐[โช{I}].
+lemma tif_atom: โI. ๐โฆโช{I}โฆ.
/2 width=4/ qed.
-lemma tif_abst: โV,T. ๐[V] โ ๐[T] โ ๐[โV.T].
+lemma tif_abst: โV,T. ๐โฆVโฆ โ ๐โฆTโฆ โ ๐โฆโV.Tโฆ.
#V #T #HV #HT #H
elim (trf_inv_abst โฆ H) -H /2 width=1/
qed.
-lemma tif_appl: โV,T. ๐[V] โ ๐[T] โ ๐[T] โ ๐[โV.T].
+lemma tif_appl: โV,T. ๐โฆVโฆ โ ๐โฆTโฆ โ ๐โฆTโฆ โ ๐โฆโV.Tโฆ.
#V #T #HV #HT #S #H
elim (trf_inv_appl โฆ H) -H /2 width=1/
qed.