(* Basic_2A1: uses: fpbg_fleq_trans *)
lemma fpbg_feqg_trans (S) (G) (L) (T):
reflexive … S → symmetric … S →
- â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« > â\9dªG,L,Tâ\9d« →
- â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© > â\9d¨G,L,Tâ\9d© →
+ â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
/3 width=8 by fpbg_fpb_trans, feqg_fpb/ qed-.
(* Basic_2A1: uses: fleq_fpbg_trans *)
lemma feqg_fpbg_trans (S) (G) (L) (T):
reflexive … S → symmetric … S →
- â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG,L,Tâ\9d« →
- â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« > â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G,L,Tâ\9d© →
+ â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© > â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
/3 width=8 by fpb_fpbg_trans, feqg_fpb/ qed-.
(* Properties with generic equivalence for terms ****************************)
lemma fpbg_teqg_div (S):
reflexive … S → symmetric … S →
- â\88\80G1,G2,L1,L2,T1,T. â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,Tâ\9d« →
- â\88\80T2. T2 â\89\9b[S] T â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G2,L1,L2,T1,T. â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,Tâ\9d© →
+ â\88\80T2. T2 â\89\9b[S] T â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
/4 width=8 by fpbg_feqg_trans, teqg_feqg, teqg_sym/ qed-.
(* Advanced inversion lemmas of parallel rst-computation on closures ********)
(* Basic_2A1: was: fpbs_fpbg *)
lemma fpbs_inv_fpbg:
- â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d« →
- â\88¨â\88¨ â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d«
- | â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d© →
+ â\88¨â\88¨ â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d©
+ | â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
#G1 #G2 #L1 #L2 #T1 #T2 #H
elim (fpbs_inv_fpbc_sn … H) -H
[ /2 width=1 by or_introl/
(* Basic_2A1: this was the definition of fpbg *)
lemma fpbg_inv_fpbc_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
- â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d« →
- â\88\83â\88\83G,L,T. â\9dªG1,L1,T1â\9d« â\89» â\9dªG,L,Tâ\9d« & â\9dªG,L,Tâ\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+ â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d© →
+ â\88\83â\88\83G,L,T. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G,L,Tâ\9d© & â\9d¨G,L,Tâ\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
#G1 #G2 #L1 #L2 #T1 #T2 #H
elim (fpbg_inv_gen … H) -H #G3 #L3 #T3 #G4 #L4 #T4 #H13 #H34 #H42
elim (fpbs_inv_fpbc_sn … H13) -H13
(* Advanced properties of parallel rst-computation on closures **************)
lemma fpbs_fpb_trans:
- â\88\80F1,F2,K1,K2,T1,T2. â\9dªF1,K1,T1â\9d« â\89¥ â\9dªF2,K2,T2â\9d« →
- â\88\80G2,L2,U2. â\9dªF2,K2,T2â\9d« â\89» â\9dªG2,L2,U2â\9d« →
- â\88\83â\88\83G1,L1,U1. â\9dªF1,K1,T1â\9d« â\89» â\9dªG1,L1,U1â\9d« & â\9dªG1,L1,U1â\9d« â\89¥ â\9dªG2,L2,U2â\9d«.
+ â\88\80F1,F2,K1,K2,T1,T2. â\9d¨F1,K1,T1â\9d© â\89¥ â\9d¨F2,K2,T2â\9d© →
+ â\88\80G2,L2,U2. â\9d¨F2,K2,T2â\9d© â\89» â\9d¨G2,L2,U2â\9d© →
+ â\88\83â\88\83G1,L1,U1. â\9d¨F1,K1,T1â\9d© â\89» â\9d¨G1,L1,U1â\9d© & â\9d¨G1,L1,U1â\9d© â\89¥ â\9d¨G2,L2,U2â\9d©.
#F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
[ #H12 #G2 #L2 #U2 #H22
lapply (feqg_fpbc_trans … H12 … H22) -F2 -K2 -T2