equal
deleted
inserted
replaced
128 in |
128 in |
129 pc+1 < max_pc \\<and> |
129 pc+1 < max_pc \\<and> |
130 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> |
130 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> |
131 (ts # ts' # ST' , LT) = s'))" |
131 (ts # ts' # ST' , LT) = s'))" |
132 |
132 |
133 "wtl_OS ADD s s' max_pc pc = |
133 "wtl_OS IAdd s s' max_pc pc = |
134 (let (ST,LT) = s |
134 (let (ST,LT) = s |
135 in |
135 in |
136 pc+1 < max_pc \\<and> |
136 pc+1 < max_pc \\<and> |
137 (\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and> |
137 (\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and> |
138 ((PrimT Integer) # ST' , LT) = s'))" |
138 ((PrimT Integer) # ST' , LT) = s'))" |