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