추가 가설

Question

나는 증거가 내 가설에 내가 가진 : 나는 가설 H을 깰 기술에 붙어

... 
l0 : list 
     (list (ATrs.rule (Sig a)) * boolean * option (list positiveInteger) * 
      option cpf.dpProof) 
H: forall 
     x : list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) * 
      option cpf.dpProof, 
     In x l0 -> 
     (let (p, o) := x in 
     let (p0, _) := p in 
     let (dps, b) := p0 in 
     if b 
     then 
     match o with 
     | Some pi => bool_of_result (dpProof n R dps pi) 
     | None => false 
     end 
     else co_scc (dpg_unif_N 100 R D) dps) = true 
ci : list (ATrs.rule (Sig a)) 
Hin : In ci l1 
=========================== 
.... 

. 내가 x:list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) * option cpf.dpProof이라는 가설과 가설 Hx: In x l0을 가지고 있다면 나는 전술을 사용할 수있다 : ded (H x Hx)(let (p, ...)이 H 인 부분을 얻는다.

이 경우 ci은 x과 다른 유형이므로 H에 ded (H ci Hin)을 사용할 수 없습니다.

원하는 가설 (x 및 Hx)을 어떻게 추가 할 수 있는지 알고 싶습니다.

도움 주셔서 감사합니다.

Answer 1

당신의 상황이 l0에 대한 자세한 정보를 포함하지 않는 글쎄, 당신이 인수 한 이후, H 중 무엇을 추론 할 수 없을 것 몇 가지 x에 대한 In x l0을 입력있다.

l0이 컨텍스트와 목표에서 완전히 제약을받지 않으면 효과적으로 유형의 임의의 목록이 될 수 있으므로 In x l0 유형을 위조 할 방법이 없으므로 사용할 수 없습니다. H.

어딘가 모순이 있거나이 증거를 공격하는 다른 방법 일 수 있습니다.