mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
16 lines
433 B
Plaintext
16 lines
433 B
Plaintext
theory Test_simplify_array
|
|
use int.Int
|
|
use map.Map
|
|
goal G1 : forall x y:int. forall m: map int int.
|
|
get (set m y x) y = x
|
|
goal G2 : forall x y z t:int. forall m: map int int.
|
|
z <> x ->
|
|
get m z = y ->
|
|
get (set m x t) z = y
|
|
goal G3 : forall y t:int. forall m: map int int.
|
|
get m 0 = y ->
|
|
get (set m 1 t) 0 = y
|
|
goal G4 : forall x y:int. forall m: map int int.
|
|
get (set (set m 1 y) 0 x) 1 = y
|
|
end
|