∀ p, equal (gcd_aux_body (p+1)) (λm. λn. if (dividesb n m) then n else (gcd_aux p n (mod m n)))

Axiom axiom_gcd_aux_body_S : forall (p:nat.nat), connectives.equal (nat.nat -> nat.nat -> nat.nat) (gcd_aux_body (nat.S p)) (fun (m:nat.nat) => fun (n:nat.nat) => bool.match_bool_type (nat.nat) n (gcd_aux p n (div_mod.mod m n)) (primes.dividesb n m))

axiom axiom_gcd_aux_body_S : \forall (p:nat). (equal) (nat -> nat -> nat) ((gcd_aux_body) ((S) p)) (\lambda m : nat. \lambda n : nat. (match_bool_type) (nat) n ((gcd_aux) p n ((mod) m n)) ((dividesb) n m))

axiom axiom_gcd_aux_body_S : forall (p:nat.nat) , (((connectives.equal) ((nat.nat) -> (nat.nat) -> nat.nat)) (((gcd.gcd_aux_body) ) (((nat.S) ) (p)))) (fun (m : nat.nat) , fun (n : nat.nat) , ((((bool.match_bool_type) (nat.nat)) (n)) (((((gcd.gcd_aux) ) (p)) (n)) ((((div_mod.mod) ) (m)) (n)))) ((((primes.dividesb) ) (n)) (m)))

axiom_gcd_aux_body_S : AXIOM (FORALL(p:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.equal[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]](gcd_sttfa.gcd_aux_body(nat_sttfa_th.sttfa_S(p)))((LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](n)(gcd_sttfa.gcd_aux(p)(n)(div_mod_sttfa_th.mod(m)(n)))(primes_sttfa_th.dividesb(n)(m))))))

Printing for OpenTheory is not working at the moment.