(* Basic_2A1: uses: fpbq_fpbs *)
lemma fpb_fpbs:
- â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« →
- â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© →
+ â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
/2 width=1 by tri_inj/ qed.
lemma fpbs_strap1:
- â\88\80G1,G,G2,L1,L,L2,T1,T,T2. â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG,L,Tâ\9d« →
- â\9dªG,L,Tâ\9d« â\89½ â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G,G2,L1,L,L2,T1,T,T2. â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G,L,Tâ\9d© →
+ â\9d¨G,L,Tâ\9d© â\89½ â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
/2 width=5 by tri_step/ qed-.
lemma fpbs_strap2:
- â\88\80G1,G,G2,L1,L,L2,T1,T,T2. â\9dªG1,L1,T1â\9d« â\89½ â\9dªG,L,Tâ\9d« →
- â\9dªG,L,Tâ\9d« â\89¥ â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G,G2,L1,L,L2,T1,T,T2. â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G,L,Tâ\9d© →
+ â\9d¨G,L,Tâ\9d© â\89¥ â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
/2 width=5 by tri_TC_strap/ qed-.
(* Basic_2A1: removed theorems 3: