def step_found

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:91

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as PR

91def step_found(+t: Nat, +q: Nat, +pt: {SN.prime(t) == False{} : Bool}, +ih: {Bool.and(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t)) == True{} : Bool}) -> {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, t), t)) == True{} : Bool}:
92  +a12 = L.and_left(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t), ih)
93  +a1 = L.and_left(Nat.is_le(1n+t, q), SN.prime(q), a12)
94  +a2 = L.and_right(Nat.is_le(1n+t, q), SN.prime(q), a12)
95  +a3 = L.and_right(Bool.and(Nat.is_le(1n+t, q), SN.prime(q)), SF.no_prime(Nat.sub(q, 1n+t), 1n+t), ih)
96  +le = N.le_trans(t, 1n+t, q, N.le_succ(t), a1)
97  +es = PR.sub_split(q, t, N.succ_le_lt(t, q, a1))
98  %Equal.sym(Nat, Nat.sub(q, t), 1n+Nat.sub(q, 1n+t), es) : {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), SF.no_prime(_, t)) == True{} : Bool}
99  %Equal.sym(Bool, SN.prime(t), False{}, pt) : {Bool.and(Bool.and(Nat.is_le(t, q), SN.prime(q)), Bool.and(Bool.not(_), SF.no_prime(Nat.sub(q, 1n+t), 1n+t))) == True{} : Bool}
100  L.and_intro(Bool.and(Nat.is_le(t, q), SN.prime(q)), Bool.and(True{}, SF.no_prime(Nat.sub(q, 1n+t), 1n+t)), L.and_intro(Nat.is_le(t, q), SN.prime(q), le, a2), a3)