lemma feqg_dec (S):
(∀s1,s2. Decidable … (S s1 s2)) →
- â\88\80G1,G2,L1,L2,T1,T2. Decidable (â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d«).
+ â\88\80G1,G2,L1,L2,T1,T2. Decidable (â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d©).
#S #HS #G1 #G2 #L1 #L2 #T1 #T2
elim (eq_genv_dec G1 G2) #HnG destruct
[ elim (reqg_dec … HS L1 L2 T1) #HnL
theorem feqg_canc_sn (S):
reflexive … S → symmetric … S → Transitive … S →
- â\88\80G,G1,L,L1,T,T1. â\9dªG,L,Tâ\9d« â\89\9b[S] â\9dªG1,L1,T1â\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« â\89\9b[S] â\9dªG2,L2,T2â\9d«.
+ â\88\80G,G1,L,L1,T,T1. â\9d¨G,L,Tâ\9d© â\89\9b[S] â\9d¨G1,L1,T1â\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© â\89\9b[S] â\9d¨G2,L2,T2â\9d©.
/3 width=5 by feqg_trans, feqg_sym/ qed-.
theorem feqg_canc_dx (S):
reflexive … S → symmetric … S → Transitive … S →
- â\88\80G1,G,L1,L,T1,T. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG,L,Tâ\9d« →
- â\88\80G2,L2,T2. â\9dªG2,L2,T2â\9d« â\89\9b[S] â\9dªG,L,Tâ\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G,L1,L,T1,T. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G,L,Tâ\9d© →
+ â\88\80G2,L2,T2. â\9d¨G2,L2,T2â\9d© â\89\9b[S] â\9d¨G,L,Tâ\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d©.
/3 width=5 by feqg_trans, feqg_sym/ qed-.
lemma feqg_reqg_trans (S) (G2) (L) (T2):
reflexive … S → symmetric … S → Transitive … S →
- â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L,T2â\9d« →
- â\88\80L2. L â\89\9b[S,T2] L2 â\86\92 â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L,T2â\9d© →
+ â\88\80L2. L â\89\9b[S,T2] L2 â\86\92 â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d©.
#S #G2 #L #T2 #H1S #H2S #H3S #G1 #L1 #T1 #H1 #L2 #HL2
/4 width=5 by feqg_trans, feqg_intro_sn, teqg_refl/
qed-.
(* Basic_2A1: uses: feqg_tneqg_repl_dx *)
lemma feqg_tneqg_trans (S) (G1) (G2) (L1) (L2) (T):
reflexive … S → symmetric … S → Transitive … S →
- â\88\80T1. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,Tâ\9d« →
+ â\88\80T1. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,Tâ\9d© →
∀T2. (T ≛[S] T2 → ⊥) → (T1 ≛[S] T2 → ⊥).
#S #G1 #G2 #L1 #L2 #T #H1S #H2S #H3S #T1 #H1 #T2 #HnT2 #HT12
elim (feqg_inv_gen_sn … H1) -H1 #_ #_ #HnT1 -G1 -G2 -L1 -L2