changeset 5608 | a82a038a3e7a |
parent 5420 | b48ab3281944 |
child 5648 | fe887910e32e |
5607:5db9e2343ade | 5608:a82a038a3e7a |
---|---|
41 next :: nat => nat |
41 next :: nat => nat |
42 |
42 |
43 assumes |
43 assumes |
44 N_positive "0<N" |
44 N_positive "0<N" |
45 |
45 |
46 skip "id: acts" |
46 skip "Id: acts" |
47 |
47 |
48 TR2 "!!i. constrains acts (T i) (T i Un H i)" |
48 TR2 "!!i. constrains acts (T i) (T i Un H i)" |
49 |
49 |
50 TR3 "!!i. constrains acts (H i) (H i Un E i)" |
50 TR3 "!!i. constrains acts (H i) (H i Un E i)" |
51 |
51 |