Proof Step: c_0_0

name: c_0_0 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/Tutorial/0035_Message/prob_00138_003649.p' file node: fact_3_keysFor__def

Proof State Overview

proof_step c_0_0 ⊕ keysFor = ? c_0_7 ⊕ keysFor X2879 = image_nat_nat invKey collect_nat ? c_0_0->c_0_7

Input Dependencies

c_0_0

Assumptions

None

Conclusion

c_0_0

Dependents

c_0_7

Formula

( keysFor
= ( ^ [X4: set_msg] :
      ( image_nat_nat @ invKey
      @ ( collect_nat
        @ ^ [X5: nat] :
          ? [X6: msg] : ( member_msg @ ( crypt @ X5 @ X6 ) @ X4 ) ) ) ) )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/Tutorial/0035_Message/prob_00138_003649.p',fact_3_keysFor__def)