Running Anthem

Specification

composite(I*J) :- I>1, J>1. prime(I) :- I = 2..n, not composite(I).

Program

composite(I*J) :- I = 2..n, J = 2..n. prime(I) :- I = 2..n, not composite(I).

User Guide

input: n -> integer. assumption: n > 1. output: prime/1.

Proof Outline

lemma: forall M$i N$i( M$i >= 1 and N$i >= 1 -> M$i * N$i >= M$i ).