The prover does not see any problem because (recalling the meaning of the word "axiom") there is nothing to prove and because there is no fundamental reason why the prover should complain about contradictory axioms. For convenience of the hypothetical audience, a pretty print of the context in temp.zip is displayed below. (So, ":" in the report is the usual escape notation for the "is in" operator, thus not a pretty print delimiter.)
what I put here is the extraction of an example written made by JR Abrial which title is "development of a concurrent program". While reading the example, I edited the model and decide to make the proofs. At the first refinement, for the proof obligation "initialisation/inv10/INV" I met the problem isolated here.
In the available hypothesis window I had "1 : 2..4" and in the goal window "1..1+1 <: {1}
(screen capture joined)
File Added: bizarre.jpg
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The prover does not see any problem because (recalling the meaning of the word "axiom") there is nothing to prove and because there is no fundamental reason why the prover should complain about contradictory axioms. For convenience of the hypothetical audience, a pretty print of the context in temp.zip is displayed below. (So, ":" in the report is the usual escape notation for the "is in" operator, thus not a pretty print delimiter.)
CONTEXT
c
SETS
D
AXIOMS
axm1 : 1 ∈ 2‥4
axm2 : 5 ∈ 2‥4
axm3 : 5 ∈ {2,3,4}
axm4 : 0 ∈ 2‥4
axm5 : 0 ∈ 2‥1
END
screen capture
what I put here is the extraction of an example written made by JR Abrial which title is "development of a concurrent program". While reading the example, I edited the model and decide to make the proofs. At the first refinement, for the proof obligation "initialisation/inv10/INV" I met the problem isolated here.
In the available hypothesis window I had "1 : 2..4" and in the goal window "1..1+1 <: {1}
(screen capture joined)
File Added: bizarre.jpg
screen capture
screen capture
there was no problem.