PPC PPC114-F "Fre PodWW Wse Rfe PodRR Fre Rfi DpAddrdR" {0:r2=z; 0:r4=x; 0:r6=a; 1:r2=x; 1:r4=c; 1:r6=a; 2:r2=x; 2:r4=y; 2:r6=b; 2:r10=c; 3:r2=y; 3:r6=z; 3:r8=a; 3:r10=b;} P0 | P1 | P2 | P3 ; li r5,2 | li r3,1 | li r5,1 | lwz r7,0(r8) ; li r1,1 | li r1,2 | stw r5,0(r6) | sync ; stw r1,0(r2) | stw r3,0(r4) | lwz r7,0(r6) | lwz r9,0(r10) ; lwsync | lwsync | sync | li r1,1 ; li r3,1 | stw r1,0(r2) | lwz r1,0(r2) | stw r1,0(r2) ; stw r3,0(r4) | lwsync | sync | lwz r3,0(r2) ; lwsync | li r5,1 | xor r8,r7,r7 | sync ; stw r5,0(r6) | stw r5,0(r6) | lwz r3,0(r4) | xor r4,r3,r3 ; | | sync | lwzx r5,r4,r6 ; | | lwzx r9,r8,r10 | ; forall (2:r7=1 /\ 3:r3=1 /\ (2:r3=1 /\ (2:r9=1 /\ (3:r5=1 /\ (3:r9=1 /\ (a=2 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ x=1 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0))) \/ a=1 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ x=1 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)))) \/ 3:r9=0 /\ (a=2 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ 3:r7=0 \/ 2:r1=0 /\ 3:r7=0) \/ x=1 /\ (2:r1=2 /\ (3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0)) \/ a=1 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0) \/ x=1 /\ (2:r1=2 /\ 3:r7=0 \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0)))) \/ 3:r5=0 /\ (3:r7=1 /\ a=2 /\ x=1 /\ (3:r9=1 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0) \/ 3:r9=0 /\ (2:r1=2 \/ 2:r1=1)) \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 /\ (x=2 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0) \/ x=1 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0)) \/ a=1 /\ (x=2 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0) \/ x=1 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0))) \/ 3:r9=0 /\ (a=2 /\ (x=2 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0) \/ x=1 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0)) \/ a=1 /\ (x=2 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0) \/ x=1 /\ (2:r1=2 \/ 2:r1=1 \/ 2:r1=0)))))) \/ 2:r9=0 /\ (2:r1=1 /\ x=2 /\ (3:r5=1 /\ (3:r7=2 /\ a=1 /\ (3:r9=1 \/ 3:r9=0) \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 \/ a=1) \/ 3:r9=0 /\ (a=2 \/ a=1))) \/ 3:r5=0 /\ 3:r7=0 /\ (3:r9=1 /\ (a=2 \/ a=1) \/ 3:r9=0 /\ (a=2 \/ a=1))) \/ 2:r1=0 /\ (3:r5=1 /\ (3:r7=2 /\ 3:r9=1 /\ a=1 /\ x=2 \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)) \/ 3:r9=0 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)))) \/ 3:r5=0 /\ 3:r7=0 /\ (3:r9=1 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)) \/ 3:r9=0 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)))))) \/ 2:r3=0 /\ (2:r9=1 /\ (3:r5=1 /\ (3:r9=1 /\ (a=2 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ x=1 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0))) \/ a=1 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ x=1 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)))) \/ 3:r9=0 /\ (a=2 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ 3:r7=0 \/ 2:r1=0 /\ 3:r7=0) \/ x=1 /\ (2:r1=2 /\ (3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0)) \/ a=1 /\ (x=2 /\ (2:r1=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0) \/ x=1 /\ (2:r1=2 /\ 3:r7=0 \/ 2:r1=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ 2:r1=0 /\ 3:r7=0)))) \/ 3:r5=0 /\ (2:r1=2 /\ x=1 /\ (3:r7=1 /\ a=2 /\ (3:r9=1 \/ 3:r9=0) \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 \/ a=1) \/ 3:r9=0 /\ (a=2 \/ a=1))) \/ 2:r1=0 /\ (3:r7=1 /\ 3:r9=1 /\ a=2 /\ x=1 \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)) \/ 3:r9=0 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)))))) \/ 2:r9=0 /\ (2:r1=1 /\ 3:r5=1 /\ x=2 /\ (3:r9=1 /\ (a=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ a=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ 3:r9=0 /\ (3:r7=2 /\ a=1 \/ 3:r7=0 /\ (a=2 \/ a=1))) \/ 2:r1=0 /\ (3:r5=1 /\ (3:r9=1 /\ (a=2 /\ (x=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ x=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0)) \/ a=1 /\ (x=2 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0) \/ x=1 /\ (3:r7=2 \/ 3:r7=1 \/ 3:r7=0))) \/ 3:r9=0 /\ 3:r7=0 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1))) \/ 3:r5=0 /\ (3:r7=1 /\ 3:r9=1 /\ a=2 /\ x=1 \/ 3:r7=0 /\ (3:r9=1 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)) \/ 3:r9=0 /\ (a=2 /\ (x=2 \/ x=1) \/ a=1 /\ (x=2 \/ x=1)))))))))