equal
deleted
inserted
replaced
767 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
767 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
768 same_inode_nil_prop cm2smsg_nil_prop |
768 same_inode_nil_prop cm2smsg_nil_prop |
769 dest:init_same_inode_prop1 |
769 dest:init_same_inode_prop1 |
770 split:option.splits) |
770 split:option.splits) |
771 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
771 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
772 apply (drule is_init_file_prop1, simp add:init_files_props) |
|
773 done |
772 done |
774 |
773 |
775 lemma s2ss_nil_prop: |
774 lemma s2ss_nil_prop: |
776 "s2ss [] = init_static_state" |
775 "s2ss [] = init_static_state" |
777 using co2sobj_nil_prop init_alive_prop |
776 using co2sobj_nil_prop init_alive_prop |