StepUsing
true=> prime(2) ;
integer(Y) and any(Y) and (factor(Y,2)) and Y > 0=> Y = 1 or Y = 2 ; Deduction prime
integer(Y) and any(Y) and (factor(Y,2)) and Y > 0 and not Y = 0 and not 0 > Y=> Y = 1 or Y = 2 ; Induction ordering
integer(Y) and any(Y) and true=> not ((factor(Y,2)) and Y > 0 and not Y = 0 and not 0 > Y and not Y = 1 and not Y = 2) ; Inversion
integer(Y) and any(Y) and integer(V0) and exists(V0) and true=> not (Y > 0 and not Y = 0 and not 0 > Y and not Y = 1 and not Y = 2 and Y * V0 = 2) ; Induction factor
integer(Y) and any(Y) and integer(V0) and exists(V0) and true=> not (Y > 0 and not Y = 0 and not 0 > Y and not Y = 1 and not Y = 2 and Y * V0 = 2 and V0 > 0) ; Induction times_range1
integer(Y) and any(Y) and integer(V0) and exists(V0) and true=> not (Y > 0 and not Y = 0 and not 0 > Y and not Y = 1 and not Y = 2 and Y * V0 = 2 and V0 > 0 and not Y > 2) ; Induction times_range2
integer(Y) and any(Y) and integer(V0) and exists(V0) and true=> not (Y > 0 and not Y = 0 and not 0 > Y and not Y = 1 and not Y = 2 and Y * V0 = 2 and V0 > 0 and not Y > 2 and not V0 > 2) ; Induction times_range2
true; Exhaustion