Transparent foo bar.
and if bar does not exist, foo is set opaque.
1. | A=B if A¾®biB | |
2. | Sx:A.B=Sy:A.B[x¬y] if yÏFV(Sx:A.B) | |
3. | Px:A.B=Py:A.B[x¬y] if yÏFV(Px:A.B) | |
4. | Sx:A.B=Sx:B.A if xÏFV(A,B) | |
5. | Sx:(Sy:A.B).C=Sx:A.Sy:B[y¬x].C[x¬(x,y)] | |
6. | Px:(Sy:A.B).C=Px:A.Py:B[y¬x].C[x¬(x,y)] | |
7. | Px:A.Sy:B.C=Sy:(Px:A.B).(Px:A.C[y¬(yx)] | |
8. | Sx:A.unit=A | |
9. | Sx:unit.A=A[x¬tt] | |
10. | Px:A.unit=unit | |
11. | Px:unit.A=A[x¬tt] |