(* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
lemma fsb_inv_csx:
- â\88\80G,L,T. â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d« â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T.
+ â\88\80G,L,T. â\89¥ð\9d\90\92 â\9d¨G,L,Tâ\9d© â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T.
#G #L #T #H @(fsb_ind … H) -G -L -T
/5 width=1 by csx_intro, cpx_fpbc/
qed-.
(* Propreties with context-sensitive stringly rt-normalizing terms **********)
lemma csx_fsb_fpbs:
- â\88\80G1,L1,T1. â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
- â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d« â\86\92 â\89¥ð\9d\90\92 â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,L1,T1. â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+ â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d© â\86\92 â\89¥ð\9d\90\92 â\9d¨G2,L2,T2â\9d©.
#G1 #L1 #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
#G0 #L0 #T0 #IHu #H10
qed.
lemma csx_fsb (G) (L) (T):
- â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d«.
+ â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\89¥ð\9d\90\92 â\9d¨G,L,Tâ\9d©.
/2 width=5 by csx_fsb_fpbs/ qed.
(* Advanced eliminators *****************************************************)
lemma csx_ind_fpbc (Q:relation3 …):
(∀G1,L1,T1.
- â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
- (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
+ â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+ (â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d© → Q G2 L2 T2) →
Q G1 L1 T1
) →
- â\88\80G,L,T. â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T → Q G L T.
+ â\88\80G,L,T. â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind/ qed-.
lemma csx_ind_fpbg (Q:relation3 …):
(∀G1,L1,T1.
- â\9dªG1,L1â\9d« ⊢ ⬈*𝐒 T1 →
- (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
+ â\9d¨G1,L1â\9d© ⊢ ⬈*𝐒 T1 →
+ (â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d© → Q G2 L2 T2) →
Q G1 L1 T1
) →
- â\88\80G,L,T. â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 T → Q G L T.
+ â\88\80G,L,T. â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 T → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.