50 ==> (c0 ;; c1, s) -[eval]-> s1" |
50 ==> (c0 ;; c1, s) -[eval]-> s1" |
51 |
51 |
52 IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] |
52 IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] |
53 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
53 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
54 |
54 |
55 IfFalse "[| (e,s) -|[eval]-> (1',s'); (c1,s') -[eval]-> s1 |] |
55 IfFalse "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] |
56 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
56 ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" |
57 |
57 |
58 WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1" |
58 WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1" |
59 |
59 |
60 WhileTrue "[| (e,s) -|[eval]-> (0,s1); |
60 WhileTrue "[| (e,s) -|[eval]-> (0,s1); |
61 (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] |
61 (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] |
62 ==> (WHILE e DO c, s) -[eval]-> s3" |
62 ==> (WHILE e DO c, s) -[eval]-> s3" |
63 end |
63 end |