:: deftheorem Def4 defines transitions_of SURREALI:def 4 :
for x being object
for Inv, b₃ being Function holds
( b₃ = transitions_of (x,Inv) iff ( dom b₃ = NAT & b₃ . 0 = 1_No & ( for k being Nat holds
( b₃ . k is pair & (b₃ . (k + 1)) `1 = ((L_ (b<sub>3</sub> . k)) \/ (divset ((L_ (b<sub>3</sub> . k)),x,(R_ x),Inv))) \/ (divset ((R_ (b<sub>3</sub> . k)),x,(L_ x),Inv)) & (b<sub>3</sub> . (k + 1)) `2 = ((R_ (b₃ . k)) \/ (divset ((L_ (b₃ . k)),x,(L_ x),Inv))) \/ (divset ((R_ (b₃ . k)),x,(R_ x),Inv)) ) ) ) );