= repository_nav ontology.repository, :ontologies

= ontology_nav ontology, :theorems

%h3

= link_to theorem, url_for(theorem)

= render partial: 'theorems/proof_status', locals: {proof_status: theorem.proof_status}

- unless State::TERMINAL_STATES.include?(theorem.state)

= render partial: '/shared/state', locals: {resource: theorem}

%h4

= t('proof_attempts.theorem_definition', theorem: theorem)

%p= theorem.text

- if theorem.provable

%h4 Proof Attempts

- if can?(:write, parent.repository)

= link_to t('theorems.show.prove'), url_for([theorem, :prove]), class: 'btn btn-primary'

%div

- if collection.empty?

= t('theorems.show.proof_attempts_empty')

- else

%table

%thead

%tr

%th= t('proof_attempts.index.number')

%th= t('proof_attempts.index.date')

%th= t('proof_attempts.index.time_taken')

%th= t('proof_attempts.index.prover')

%th= t('proof_attempts.index.status')

%th= t('state')

- collection.latest.each do |proof_attempt|

%tr

%td= link_to proof_attempt.number, proof_attempt.locid

%td

= link_to proof_attempt.locid do

%span.timestamp= proof_attempt.created_at

%td= t('proof_attempts.result.time_taken.text', time_taken: proof_attempt.time_taken)

%td= used_or_configured_prover(proof_attempt)

%td= render partial: 'theorems/proof_status', locals: {proof_status: proof_attempt.proof_status}

%td= render partial: 'shared/state_tag', locals: {resource: proof_attempt}

- else

%p= t('theorems.show.unprovable')