JKU LIT Project LogTechEdu
RISCAL Web Interface
Submitter:
0
of 1 grade points have been earned so far.
Silent:
Nondeterminism:
Multithreaded:
Threads:
// enter your specification val N = 5; type D = ℕ[N]; theorem T(x:D) ⇔ x > 0 ⇒ ∃y:D. y+1 = x; // provide entry point for execution proc main():() { check T; }
(no output yet)
0
of 1 grade points have been earned so far.