Definition df-eq 247

Description: Definition of channel equality. Two nilads are equivalent if, when written to an arbitrary channel, that channel behaves the same way. We measure this by seeing if we can successfully read from it.

Assertion

Ref	Expression
df-eq	⊦ (X = Y ⧟ ∇a([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1))

Detailed syntax breakdown of Definition df-eq

Step	Hyp	Ref	Expression
1		nx	. . 3 nilad X
2		ny	. . 3 nilad Y
3	1, 2	weq 246	. 2 wff X = Y
4		wone 103	. . . . . 6 wff 1
5		vb	. . . . . 6 var b
6		va	. . . . . . 7 var a
7	6	nvar 203	. . . . . 6 nilad a
8	4, 5, 7	wre 205	. . . . 5 wff [a ≫ b] 1
9	8, 7, 1	wse 204	. . . 4 wff [a ≪ X] [a ≫ b] 1
10	8, 7, 2	wse 204	. . . 4 wff [a ≪ Y] [a ≫ b] 1
11	9, 10	wlb 55	. . 3 wff ([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1)
12	11, 6	wnnu 242	. 2 wff ∇a([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1)
13	3, 12	wlb 55	1 wff (X = Y ⧟ ∇a([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1))

This definition is referenced by: (None)