include "basic_2/reduction/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
include "basic_2/reduction/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
[ //
| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
#Kd #V1d #HLKd #HV1s #HV1sd
[ //
| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
#Kd #V1d #HLKd #HV1s #HV1sd
@(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
/4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
/3 width=1 by llpx_sn_flat/
| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
@(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
/4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
/3 width=1 by llpx_sn_flat/
| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
#HV1 #H elim (llpx_sn_inv_bind_O … H) -H
| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
#HV1 #H elim (llpx_sn_inv_bind_O … H) -H
| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
#HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
#HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
#HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
#HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)