Proof Step: c_0_37

name: c_0_37 syntax: thf role: negated_conjecture inference: cn

Proof State Overview

proof_step c_0_0 c_0_0 c_0_33 ⊖ typings shift_type e n t2 as esk1_4 shift_type e n t2 app var n a X3 t ⊖ typing shift_type e n t2 foldl_dB_dB app var n cons_dB a X3 t c_0_0->c_0_33 c_0_1 ⊕ thesis c_0_1->c_0_33 c_0_2 ⊕ n = i c_0_2->c_0_33 c_0_36 ⊕ typing shift_type e n t2 foldl_dB_dB app var n rs t c_0_2->c_0_36 c_0_2->c_0_36 c_0_3 c_0_3 c_0_3->c_0_33 c_0_34 ⊕ typings X1 X3 esk1_4 X1 X6 X3 X4 ⊖ typing X1 foldl_dB_dB app X6 X3 X4 c_0_3->c_0_34 c_0_4 ⊕ foldl_dB_dB X37 X38 cons_dB X39 X40 = foldl_dB_dB X37 X37 X38 X39 X40 c_0_4->c_0_33 c_0_29 ⊕ foldl_dB_dB X37 X37 X6 X12 X3 = foldl_dB_dB X37 X6 cons_dB X12 X3 c_0_4->c_0_29 c_0_5 ⊕ rs = cons_dB a as c_0_35 ⊕ cons_dB a as = rs c_0_5->c_0_35 c_0_5->c_0_35 c_0_6 ⊕ typing shift_type e i t2 foldl_dB_dB app var n rs t c_0_6->c_0_36 c_0_6->c_0_36 c_0_37 ⊕ $false c_0_33->c_0_37 c_0_34->c_0_37 c_0_35->c_0_37 c_0_35->c_0_37 c_0_36->c_0_37 c_0_36->c_0_37 c_0_29->c_0_37

Input Dependencies

c_0_0 c_0_1 c_0_2 c_0_3 c_0_4 c_0_5 c_0_6

Assumptions

c_0_33 c_0_34 c_0_35 c_0_36 c_0_29 c_0_35 c_0_36

Conclusion

c_0_37

Dependents

None

Formula

$false

Source

inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_34]),c_0_35]),c_0_36]),c_0_29]),c_0_35]),c_0_36])])

Useful Info

[proof]