1 | 5. x,y,z:|E| List. P(x)  P(y)  ( x x.( y y. (x =msg=(E) y))) & z = (x @ y)  P(z) 6. safetyR(E) preserves P 7. safetyR(E) preserves I 8. tr:|E| List.
I(tr) 
tr = nil 
( L_1,L_2:|E| List.
tr = (L_1 @ L_2)
& L_2 = nil
& ( x L_1.( y L_2. (x =msg=(E) y)))
& ( m:Label. ( x L_2.tag(E)(x) = m))) 9. n:  10. 0 < n 11. tr:|E| List. ||tr|| n-1  ( m:Label. P( < tr > _m))  I(tr)  P(tr) 12. tr: |E| List 13. ||tr|| n 14. tr = nil 15. m:Label. P( < tr > _m) 16. I(tr) 17. L_1: |E| List 18. L_2: |E| List 19. tr = (L_1 @ L_2) 20. L_2 = nil 21. ( x L_1.( y L_2. (x =msg=(E) y))) 22. m: Label 23. ( x L_2.tag(E)(x) = m) P(L_1) |
2 | 5. x,y,z:|E| List. P(x)  P(y)  ( x x.( y y. (x =msg=(E) y))) & z = (x @ y)  P(z) 6. safetyR(E) preserves P 7. safetyR(E) preserves I 8. tr:|E| List.
I(tr) 
tr = nil 
( L_1,L_2:|E| List.
tr = (L_1 @ L_2)
& L_2 = nil
& ( x L_1.( y L_2. (x =msg=(E) y)))
& ( m:Label. ( x L_2.tag(E)(x) = m))) 9. n:  10. 0 < n 11. tr:|E| List. ||tr|| n-1  ( m:Label. P( < tr > _m))  I(tr)  P(tr) 12. tr: |E| List 13. ||tr|| n 14. tr = nil 15. m:Label. P( < tr > _m) 16. I(tr) 17. L_1: |E| List 18. L_2: |E| List 19. tr = (L_1 @ L_2) 20. L_2 = nil 21. ( x L_1.( y L_2. (x =msg=(E) y))) 22. m: Label 23. ( x L_2.tag(E)(x) = m) P(L_2) |