(* *)
(**************************************************************************)
-include "basic_2/static/gcp_aaa.ma".
+include "static_2/static/gcp_aaa.ma".
include "basic_2/rt_computation/cpxs_aaa.ma".
include "basic_2/rt_computation/csx_gcp.ma".
include "basic_2/rt_computation/csx_gcr.ma".
(* Main properties with atomic arity assignment *****************************)
-theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
-#h #o #G #L #T #A #H
-@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H)
+theorem aaa_csx: ∀h,G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
+#h #G #L #T #A #H
+@(gcr_aaa … (csx_gcp h) (csx_gcr h) … H)
qed.
(* Advanced eliminators *****************************************************)
-fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
- (â\88\80T1. â¦\83G, Lâ¦\84 ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 â\86\92 â\8a¥) â\86\92 R T2) â\86\92 R T1
+fact aaa_ind_csx_aux: ∀h,G,L,A. ∀Q:predicate term.
+ (â\88\80T1. â\9dªG,Lâ\9d« ⊢ T1 ⁝ A →
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 Q T2) â\86\92 Q T1
) →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 Q T.
+#h #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
qed-.
-lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
- (â\88\80T1. â¦\83G, Lâ¦\84 ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 â\86\92 â\8a¥) â\86\92 R T2) â\86\92 R T1
+lemma aaa_ind_csx: ∀h,G,L,A. ∀Q:predicate term.
+ (â\88\80T1. â\9dªG,Lâ\9d« ⊢ T1 ⁝ A →
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 Q T2) â\86\92 Q T1
) →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 R T.
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 Q T.
/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
-fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
- (â\88\80T1. â¦\83G, Lâ¦\84 ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 â\86\92 â\8a¥) â\86\92 R T2) â\86\92 R T1
+fact aaa_ind_csx_cpxs_aux: ∀h,G,L,A. ∀Q:predicate term.
+ (â\88\80T1. â\9dªG,Lâ\9d« ⊢ T1 ⁝ A →
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 Q T2) â\86\92 Q T1
) →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 Q T.
+#h #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
qed-.
(* Basic_2A1: was: aaa_ind_csx_alt *)
-lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
- (â\88\80T1. â¦\83G, Lâ¦\84 ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 â\86\92 â\8a¥) â\86\92 R T2) â\86\92 R T1
+lemma aaa_ind_csx_cpxs: ∀h,G,L,A. ∀Q:predicate term.
+ (â\88\80T1. â\9dªG,Lâ\9d« ⊢ T1 ⁝ A →
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 Q T2) â\86\92 Q T1
) →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 R T.
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 Q T.
/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.